proposition: Lemma sum_sym : forall A B C D E F, SumV A B C D E F -> SumV C D A B E F.
proof: Proof. intros. unfold SumV in *. assert(HH:=vector_construction C D B). ex_and HH D'. assert(HH:= (H D' H0)). clear H. assert(EqV C B D D'). apply eqv_permut. assumption. assert(EqV A D B D'0). apply eqv_permut. assumption. induction (eq_dec_points A D'0). subst D'0. apply eqv_comm in H1. assert(HP:= (eqv_mid B A D H1)). unfold EqV in H0. induction H0. apply plg_mid in H0. ex_and H0 M. assert( A = M). apply (l7_17 B D). apply HP. Midpoint. subst M. apply mid_eqv in H0. apply (eqv_trans _ _ A D'). apply H0. assumption. spliter. subst D. subst D'. apply (eqv_trans _ _ A B). apply eqv_sym. apply eqv_comm. apply H1. assumption. induction H0; induction H1. apply plg_mid in H0. apply plg_mid in H1. ex_and H0 M0. ex_and H1 M1. assert(M1 = M0). apply (l7_17 B D). apply H5. Midpoint. subst M1. assert(Parallelogram A D' D'0 C). apply (mid_plg _ _ _ _ M0). left. assumption. assumption. Midpoint. assert(EqV C D'0 A D'). unfold EqV. left. apply plg_comm2. apply plg_sym. assumption. apply (eqv_trans _ _ A D'). apply H7. assumption. spliter. subst B. subst D'0. assert(EqV C D A D'). apply eqv_permut. assumption. apply (eqv_trans _ _ A D'). apply H1. assumption. spliter. subst D. subst D'. assert(EqV A B C D'0). apply eqv_permut. assumption. apply (eqv_trans _ _ A B). apply eqv_sym. apply H0. assumption. spliter. subst D. subst D'. subst B. subst D'0. apply null_vector in HH. subst F. apply eqv_trivial. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec