proposition: Lemma eqv_trans : forall A B C D E F, EqV A B C D -> EqV C D E F -> EqV A B E F.
proof: Proof. intros. unfold EqV in *. induction H; induction H0. assert(Parallelogram A B F E \/ A = B /\ D = C /\ E = F /\ A = E). apply (plg_pseudo_trans A B D C E F); auto. apply plg_comm2. assumption. induction H1. left. auto. right. tauto. spliter. subst D. subst F. induction (eq_dec_points A B). right. tauto. left. induction H. induction H. unfold TS in H. spliter. apply False_ind. apply H3. Col. apply plgf_sym in H. apply plgf_trivial_neq in H. tauto. spliter. subst B. subst D. induction H0. induction H. unfold TS in H. spliter. apply False_ind. apply H. Col. apply plgf_trivial_neq in H. right. spliter. subst F. tauto. right. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec