proposition: Lemma det1 : forall n, \det (1%:M : matrix R n n) === 1.
proof: Proof. move=> n; rewrite <- perm_mx1, det_perm_mx, odd_perm1. by rewrite/iter/=; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms