proposition: Lemma Regles_add : forall (X V R : Ensf) (a : Elt) (u : Word), Regles X V R -> dans a V -> inmonoid (union X V) u -> Regles X V (add (couple a (word u)) R).
proof: Proof. intros X V R a u R_R dans_a_V inmonoid_u_X_V_u. red in |- *. intros x dans_x_R'. cut (couple a (word u) = x :>Elt \/ dans x R). intuition. exists a. assumption. exists u; auto. apply dans_add; assumption. Qed.
imports: Ensf Words more_words need fonctions Relations