Apply mul_nat_mul_SNo with
2,
2,
λ x0 x1 . x0 = 4 leaving 3 subgoals.
Apply nat_p_omega with
2.
The subproof is completed by applying nat_2.
Apply nat_p_omega with
2.
The subproof is completed by applying nat_2.
The subproof is completed by applying unknownprop_74ac8a784913fa4a6f9da3de96c05984e11ff1600ef66d703e49d6ee22ad106d.