proposition: Lemma mx_dot1x n m (M: mx n m): 1⋅M ≡ M.
proof: Proof. intros i j. simpl. unfold mx_dot, mx_one. apply antisym. apply leq_supx. intros i' _. case eqb_ord_spec; simpl. intros <-. apply weq_leq, dot1x. intros _. rewrite dot0x. apply leq_bx. rewrite <- (leq_xsup _ _ i) by apply in_seq. rewrite eqb_refl. simpl. now rewrite dot1x. Qed.
imports: comparisons kleene sums normalisation