proposition: Lemma eq_mat_refl dim : forall (v:matrix dim), v ==m v.
proof: Proof. induction v as [a| dim a r c m] using matrix_ind. reflexivity. repeat split;try reflexivity. apply IHm. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)