proposition: Lemma d_is_good : forall q1 q2 d1 d2 : Ensf, inclus (union (injg_d1 q1 d1) (injd_d2 q2 d2)) (prodcart (union_disj q1 q2) (prodcart alph (union_disj q1 q2))).
proof: Proof. intros. apply union_inclus. apply inclus_trans with (prodcart (map injgauche q1) (prodcart alph (map injgauche q1))). unfold injg_d1 in |- *. apply inclus_tq. unfold union_disj in |- *. auto. apply inclus_trans with (prodcart (map injdroite q2) (prodcart alph (map injdroite q2))). unfold injd_d2 in |- *. apply inclus_tq. unfold union_disj in |- *. auto. Qed.
imports: Ensf Max Words Dec Reg Rat