proposition: Lemma inter_V1'_V2'_empty : inter V1' V2' empty.
proof: Proof. unfold V1', V2' in |- *; simpl in |- *. unfold inter in |- *. split; [ auto | split ]. auto. replace (map (injproducg V1) V1) with (map injgauche V1). replace (map (injproducd V2) V2) with (map injdroite V2). intros x dans_map_1 dans_map_2. elimtype (exists y : Elt, dans y V1 /\ x = injgauche y). elimtype (exists y : Elt, dans y V2 /\ x = injdroite y). intros x2 temp; elim temp; clear temp; intros dans_x2_V2 egal_x2. intros x1 temp; elim temp; clear temp; intros dans_x1_V1 egal_x1. absurd (zero = un). unfold zero, un in |- *. red in |- *. intro. cut (0 = 1 :>nat). change (0 <> 1 :>nat) in |- *. auto. change (natural_inv (natural 0) = natural_inv (natural 1) :>nat) in |- *. apply (f_equal natural_inv); assumption. apply couple_couple_inv2 with x1 x2. replace (couple x1 zero) with x. auto. apply dans_map; assumption. apply dans_map; assumption. auto. auto. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3 gram4