proposition: Lemma combine_mx_inv (a b c d : R) m (k : 'I_m) : a * d - b * c = 1 -> combine_mx a b c d k *m combine_mx d (-b) (-c) a k = 1%:M.
proof: Proof. move=> H; rewrite -combine_stepE; apply/matrixP=> i j; rewrite !mxE. case Hi: (i == 0). rewrite !mxE (eqP Hi) !eqxx !mulr0 mxE !addr0 (eq_sym 0 j). case Hj: (j == 0); first by rewrite (eqP Hj) mulr1 !mulr0 addr0 sub0r mulrN. rewrite !mulr0 !add0r addr0 (eq_sym _ j). case: (j == lift 0 k); last by rewrite !mulr0 add0r. by rewrite mulr1 mulr1n mulrN mulrC addNr. case Hj: (j == 0). rewrite !mxE (eqP Hj) Hi add0r. case Hk: (i == _); last by rewrite !mxE Hi Hk eqxx !add0r !mulr0 addr0. by rewrite !mxE !eqxx !mulr0 mulr1 !addr0 !add0r mulrN addrC mulrC addNr. case Hk: (i == _); last by rewrite !mxE Hi Hj Hk !mulr0 !add0r !addr0. rewrite !mxE (eq_sym 0 j) Hj (eqP Hk) !(eqxx,mulr0,addr0,add0r) (eq_sym _ j). case: (j == lift 0 k); last by rewrite !mulr0 addr0. by rewrite !mulr1 addrC mulrN (mulrC c) (mulrC d). Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool Arith.Wf_nat) mathcomp(eqtype ssrnat div seq path) mathcomp(ssralg fintype perm tuple choice generic_quotient) mathcomp(matrix bigop zmodp mxalgebra poly) stronglydiscrete