proposition: Lemma mat_plus_comm : forall m n (L R : matrix m n), L <+> R =m R <+> L.
proof: Proof. unfold mat_eqA. intros. unfold mat_plus, vec_plus. mat_get_simpl. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)