proposition: Lemma mx_dot_xrow n m1 m2 p (M1: mx n m1) (M2: mx n m2) (N: mx p n): N ⋅ row_mx M1 M2 ≡ row_mx (N⋅M1) (N⋅M2).
proof: Proof. intros i j. simpl. unfold mx_dot, row_mx. now case split_spec; intros i' ->. Qed.
imports: comparisons kleene sums normalisation