proposition: Lemma mx_dotA n m p q (M: mx n m) N (P: mx p q): M⋅(N⋅P) ≡ (M⋅N)⋅P.
proof: Proof. intros i j. simpl. unfold mx_dot. setoid_rewrite dotxsum. rewrite sup_swap. apply sup_weq; trivial. intro. rewrite dotsumx. apply sup_weq; trivial. intro. apply dotA. Qed.
imports: comparisons kleene sums normalisation