proposition: Lemma egcdnP m n : m > 0 -> egcdn_spec m n (egcdn m n).
proof: Proof. have [-> /= | n_gt0 m_gt0] := posnP n; first by split; rewrite // mul1n gcdn0. rewrite /egcdn; set s := (s in egcdn_rec _ _ s); pose bz := Bezout_rec n m [::]. have: n < s.+1 by []; move defSpec: (egcdn_spec bz.2 bz.1) s => Spec s. elim: s => [[]|s IHs] //= in n m (qs := [::]) bz defSpec n_gt0 m_gt0 *. case: edivnP => q r def_m; rewrite n_gt0 ltnS /= => lt_rn le_ns1. case: posnP => [r0 {s le_ns1 IHs lt_rn}|r_gt0]; last first. by apply: IHs => //=; [rewrite natTrecE -def_m | rewrite (leq_trans lt_rn)]. rewrite {r}r0 addn0 in def_m; set b := odd _; pose d := gcdn m n. pose km := ~~ b : nat; pose kn := if b then 1 else q.-1. rewrite [bz in Spec bz](_ : _ = Bezout_rec km kn qs); last first. by rewrite /kn /km; case: (b) => //=; rewrite natTrecE addn0 muln1. have def_d: d = n by rewrite /d def_m gcdnC gcdnE modnMl gcd0n -[n]prednK. have: km * m + 2 * b * d = kn * n + d. rewrite {}/kn {}/km def_m def_d -mulSnr; case: b; rewrite //= addn0 mul1n. by rewrite prednK //; apply: dvdn_gt0 m_gt0 _; rewrite def_m dvdn_mulr. have{def_m}: kn * d <= m. have q_gt0 : 0 < q by rewrite def_m muln_gt0 n_gt0 ?andbT in m_gt0. by rewrite /kn; case b; rewrite def_d def_m leq_pmul2r // leq_pred. have{def_d}: km * d <= n by rewrite -[n]mul1n def_d leq_pmul2r // leq_b1. move: km {q}kn m_gt0 n_gt0 defSpec; rewrite {}/b {}/d {}/bz. elim: qs m n => [|q qs IHq] n r kn kr n_gt0 r_gt0 /=. set d := gcdn n r; rewrite mul0n addn0 => <- le_kn_r _ def_d; split=> //. have d_gt0: 0 < d by rewrite gcdn_gt0 n_gt0. have /ltn_pmul2l<-: 0 < kn by rewrite -(ltn_pmul2r n_gt0) def_d ltn_addl. by rewrite def_d -addn1 leq_add // mulnCA leq_mul2l le_kn_r orbT. rewrite !natTrecE; set m := _ + r; set km := _ + kn; pose d := gcdn m n. have ->: gcdn n r = d by rewrite [d]gcdnC gcdnMDl. have m_gt0: 0 < m by rewrite addn_gt0 r_gt0 orbT. have d_gt0: 0 < d by rewrite gcdn_gt0 m_gt0. move=> {}/IHq IHq le_kn_r le_kr_n def_d; apply: IHq => //; rewrite -/d. by rewrite mulnDl leq_add // -mulnA leq_mul2l le_kr_n orbT. apply: (@addIn d); rewrite mulnDr -addnA addnACA -def_d addnACA mulnA. rewrite -!mulnDl -mulnDr -addnA [kr * _]mulnC; congr addn. by rewrite addnC addn_negb muln1 mul2n addnn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)