proposition: Lemma epsilon_mx_str: forall n (M: rmx n n), epsilon_mx (M^*) ≡ (epsilon_mx M)^*.
proof: Proof. apply (mx_str_ind' (fun n M sM => epsilon_mx sM ≡ (epsilon_mx M)^*)). - intros n ? ? H ? ? H'. now rewrite H, H'. - intros ? i. elim (ord_0_empty i). - intro M. rewrite mx_str_1. intros i j. unfold epsilon_mx, scal_mx, mx_scal, mx_map. now rewrite str_eps. - intros n m a b c d e be ec f fbe ecf He Hf. unfold epsilon_mx. rewrite 2mx_map_blk, mx_str_blk. fold (epsilon_mx). assert (H1: (epsilon_mx (a+be⋅c))^* ≡ (epsilon_mx a + epsilon_mx b ⋅ (epsilon_mx d)^* ⋅ epsilon_mx c) ^*) by (unfold be; rewrite epsilon_mx_pls, 2epsilon_mx_dot, He; reflexivity). apply blk_mx_weq. + rewrite Hf. exact H1. + unfold fbe, be. now rewrite 2epsilon_mx_dot, He, Hf, H1. + unfold ecf, ec. now rewrite 2epsilon_mx_dot, He, Hf, H1. + unfold ecf, be, ec. now rewrite epsilon_mx_pls, 4epsilon_mx_dot, He, Hf, H1. Qed.
imports: monoid regex lset boolean sups matrix_ext normalisation