proposition: Lemma kapP : gcdr a (gcdr b c) %= 1 -> exists p q, coprimer (p * a) (p * b + q * c).
proof: Proof. case: (smithP (mx2 a b 0 c))=> /= P d Q; rewrite -dvdr1. set D := diag_mx_seq _ _ _ => heq hsorted P_unitmx Q_unitmx Hgcd. exists (P 0 0); exists (P 0 1). suff [[x y /=]] : exists xy, xy.1 * (P 0 0 * a) + xy.2 * (P 0 0 * b + P 0 1 * c) %= 1. rewrite -unitd1; case/unitrP=> z [hz1 _]. by apply/coprimerP; exists (z*x,z*y); rewrite -!mulrA -mulrDr. exists (Q 0 0,Q 1 0)=> /=. suff : (D 0 0) \is a GRing.unit. rewrite -unitd1 -heq; do 2!(rewrite !mxE big_ord_recl big_ord1). rewrite big_ord_recl big_ord1 mx2_E00. have -> : lift 0 0 = 1 :> 'I_2 by apply/ord_inj. by rewrite mx2_E10 mx2_E11 mx2_E01 mulr0 addr0 mulrC [_ * Q 1 0]mulrC. rewrite unitd1 -dvdr1; apply/(dvdr_trans _ Hgcd). have Hij : forall i j, D 0 0 %| (mx2 a b 0 c) i j. rewrite (canRL (mulKmx P_unitmx) (canRL (mulmxK Q_unitmx) heq)). apply: dvdr_mulmxl; apply: dvdr_mulmxr=> i j; rewrite !mxE eqxx /=. case: eqP => _ /=; last by rewrite mulr0n dvdr0. by rewrite !mulr1n; exact: sorted_nth0. rewrite !dvdr_gcd; move: (Hij 0 0) (Hij 0 1) (Hij 1 1). by rewrite mx2_E00 mx2_E01 mx2_E11=> -> -> ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype matrix mxalgebra bigop zmodp perm choice) dvdring mxstructure minor stronglydiscrete coherent edr