proposition: Lemma unitrig1 : unitrig (fun x y => (x == y)%:R).
proof: Proof. apply/unitrigP; split => [u | u v] /=; first by rewrite eq_refl. by case: (v =P u) => [-> |] //=; rewrite eq_refl. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat order) mathcomp(fintype bigop ssralg) mathcomp(finset fingroup perm matrix)