proposition: Lemma eq_mat_refl dim : forall (v:matrix dim), v ==m v.
proof: Proof. apply eq_mat_refl with (eq:=eq). apply eq_Equivalence. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)