proposition: Lemma is_nfa_nfa A: is_nfa (to_nfa A).
proof: Proof. split. intros ? ?. simpl. unfold mx_fun. case eqb_ord; constructor. split. intros ? ?. simpl. rewrite mx_sup. apply is_pure_sup. intros. unfold mx_fun. case eqb_ord; constructor. intros ? ?. apply is_01_ofbool. Qed.
imports: positives comparisons kleene regex rmx sums matrix_ext prop normalisation