proposition: Lemma sol_odd a b n : sol (2 * n + 1) a b = (a == 2 ^ n) && (b == 2 ^ n).
proof: Proof. apply/idP/idP=> [|/andP[/eqP-> /eqP->]]; last first. by rewrite /sol !expn_gt0/= expnD muln2 addnn -expnM mulnC. elim: n => [|n IHn] in a b *; first by rewrite sol1. rewrite mulnS !add2n !addSn => solab. have [//|/negPf aNodd /negPf bNodd] := andP (sol_are_even _ solab). rewrite /sol -[a]odd_double_half -[b]odd_double_half aNodd bNodd. by rewrite -!muln2 !expnSr !eqn_mul2r IHn// solSS. Qed.
imports: mathcomp(all_ssreflect)