proposition: Lemma eqv_sum : forall A B C A' B' C', EqV A B A' B' -> EqV B C B' C' -> EqV A C A' C'.
proof: Proof. intros. unfold EqV in *. induction H. induction H0. apply plg_comm2 in H. apply plg_permut in H. apply plg_permut in H0. apply plg_sym in H0. assert(HH:= plg_pseudo_trans A A' B' B C C' H H0). induction HH. left. apply plg_permut. apply plg_comm2. assumption. spliter. right. subst A'. subst C'. tauto. spliter. subst C. subst C'. left. assumption. spliter. subst B. subst B'. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec