proposition: Lemma Mmult_assoc {n m k l} : forall (A : matrix n m) (B : matrix m k) (C : matrix k l), Mmult A (Mmult B C) = Mmult (Mmult A B) C.
proof: Proof. intros A B C. apply mk_matrix_ext => n' l' Hn' Hl'. unfold Mmult at 1. - transitivity (sum_n (fun l0 : nat => mult (coeff_mat zero A n' l0) (sum_n (fun l1 : nat => mult (coeff_mat zero B l0 l1) (coeff_mat zero C l1 l')) (pred k))) (pred m)). destruct m ; simpl. unfold coeff_mat ; simpl. by rewrite 2!mult_zero_l. apply sum_n_m_ext_loc ; simpl => m' [ _ Hm']. apply f_equal. rewrite coeff_mat_bij //. by apply Nat.lt_succ_r, Hm'. - transitivity (sum_n (fun l0 : nat => sum_n (fun l1 : nat => mult (coeff_mat zero A n' l0) (mult (coeff_mat zero B l0 l1) (coeff_mat zero C l1 l'))) (pred k)) (pred m)). destruct m ; simpl. rewrite /sum_n !sum_n_n. unfold coeff_mat ; simpl. rewrite mult_zero_l. rewrite sum_n_m_mult_l. by rewrite mult_zero_l. apply sum_n_m_ext_loc ; simpl => m' [_ Hm']. apply sym_eq, sum_n_m_mult_l. rewrite sum_n_switch. destruct k ; simpl. unfold coeff_mat ; simpl. rewrite mult_zero_l. rewrite /sum_n sum_n_m_mult_r. by rewrite mult_zero_r. apply sum_n_m_ext_loc => k' [_ Hk']. transitivity (mult (sum_n (fun l1 : nat => mult (coeff_mat zero A n' l1) (coeff_mat zero B l1 k')) (pred m)) (coeff_mat zero C k' l')). rewrite -sum_n_m_mult_r. apply sum_n_m_ext_loc => m' [_ Hm']. apply mult_assoc. apply f_equal2. unfold Mmult ; rewrite coeff_mat_bij //. by apply Nat.lt_succ_r. by []. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub