proposition: Lemma matrix : monoid Mat2.
proof: Proof. refine (mkmonoid Mat2 Id2 Mat_mult _ _ _). exact Mat_assoc. simple induction a. intros M13 M14 M23 M24. unfold Id2, Mat_mult in |- *; simpl in |- *. repeat elim Zplus_0_r_reverse. case M13; case M14; case M23; case M24; auto. simple induction a. intros. unfold Id2, Mat_mult in |- *; simpl in |- *. repeat elim Zmult_0_r_reverse. repeat rewrite Zmult_1_r. simpl in |- *; repeat elim Zplus_0_r_reverse. auto with arith. Defined.
imports: monoid Arith ZArith Compare_dec fmpc