proposition: Lemma mx_dot_colx n1 n2 m p (M1: mx n1 m) (M2: mx n2 m) (N: mx m p): col_mx M1 M2 ⋅ N ≡ col_mx (M1⋅N) (M2⋅N).
proof: Proof. intros i j. simpl. unfold mx_dot, col_mx. now case split_spec; intros i' ->. Qed.
imports: comparisons kleene sums normalisation