proposition: Lemma is_mono_u_X_V1_injproducg_V1 : is_mono (union X V1) (injproducg V1).
proof: Proof. unfold is_mono in |- *. intros x y dans_x_u dans_y_u. elimtype (dans x X \/ dans x V1). intro dans_x. replace (injproducg V1 x) with x. elimtype (dans y X \/ dans y V1). intros dans_y. replace (injproducg V1 y) with y. auto. apply sym_equal; auto. intros dans_y. replace (injproducg V1 y) with (injgauche y). unfold injgauche in |- *. elim (Mots_X x dans_x). intros x0 egal_x egal2_x. absurd (word x0 = couple y zero). discriminate. rewrite egal_x; assumption. apply sym_equal; auto. auto. apply sym_equal; auto. intro dans_x. replace (injproducg V1 x) with (injgauche x). elimtype (dans y X \/ dans y V1). intros dans_y. replace (injproducg V1 y) with y. unfold injgauche in |- *. elim (Mots_X y dans_y). intros x0 egal_y egal2_y. absurd (word x0 = couple x zero). discriminate. rewrite egal2_y; assumption. apply sym_equal; auto. intro. replace (injproducg V1 y) with (injgauche y). unfold injgauche in |- *. intros. apply couple_couple_inv1 with zero zero; assumption. apply sym_equal; auto. auto. apply sym_equal; auto. auto. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3 gram4