proposition: Lemma mx_dotx1 n m (M: mx m n): M⋅1 ≡ 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, dotx1. intros _. rewrite dotx0. apply leq_bx. rewrite <- (leq_xsup _ _ j) by apply in_seq. rewrite eqb_refl. simpl. now rewrite dotx1. Qed.
imports: comparisons kleene sums normalisation