proposition: Lemma det2 (A : 'M[R]_(2,2)) : \det A = A 0 0 * A 1 1 - A 1 0 * A 0 1.
proof: Proof. rewrite (expand_det_col _ 0) !big_ord_recl big_ord0 addr0 /cofactor /=. rewrite ?(addn0,expr0,mul1r) /bump leq0n /= addn0 expr1. do 2! rewrite [X in \det X]mx11_scalar det_scalar1 /=. by rewrite !mxE !mulNr mul1r mulrN; do ?f_equal; apply/ord_inj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)