fact: Axiom transition_a_droite_2 : forall (q1 qa1 d1 q2 qd2 d2 : Ensf) (e0 x e : Elt), dans e0 (map injdroite q2) -> dans x alph -> dans (couple e0 (couple x e)) (union (pont qa1 qd2) (union (injg_d1 q1 d1) (injd_d2 q2 d2))) -> dans (couple (first e0) (couple x (first e))) d2.
imports: Ensf Max Words Dec Reg Rat