proposition: Lemma solSS n a b : sol n.+2 a b -> sol n a./2 b./2.
proof: Proof. move=> soln2ab; have [//|a_even b_even] := andP (sol_are_even _ soln2ab). rewrite /sol -[a]odd_double_half -[b]odd_double_half in soln2ab. rewrite (negPf a_even) (negPf b_even) ?add0n ?double_gt0 in soln2ab. rewrite /sol; move: soln2ab => /and3P[-> -> /=]. by rewrite -(addn2 n) expnD -!muln2 !expnMn -mulnDl eqn_mul2r. Qed.
imports: mathcomp(all_ssreflect)