proposition: Lemma det2 (R': comRingType) (M: 'M_2): (\det M: R') = M ord0 ord0 * M (lift ord0 ord0) (lift ord0 ord0) - M ord0 (lift ord0 ord0) * M (lift ord0 ord0) ord0.
proof: Proof. rewrite (expand_det_row M ord0) !big_ord_recl big_ord0 /cofactor !det_mx11. rewrite !mxE/= /bump /= !(addn0,expr0,mul1r,add0n,addr0,expr1,mulN1r,mulrN)/=. congr (_ - (_ * M _ _)). exact: val_inj. Qed.
imports: axiomsKnuth mathcomp(all_ssreflect ssralg matrix ssrnum vector reals) mathcomp(normedtype order) mathcomp.algebra_tactics(ring) mathcomp.zify(zify)