proposition: Lemma opposite_sum : forall A B C D E F, SumV A B C D E F -> SumV B A D C F E.
proof: Proof. intros. unfold SumV in *. intros D0 H0. assert(HH:=vector_construction C D B). ex_and HH D'. assert(HH:= (H D' H1)). clear H. assert(EqV D' B A D0). apply (eqv_trans _ _ D C). apply eqv_sym. apply eqv_comm. apply H1. assumption. apply eqv_permut in H. eapply (eqv_trans _ _ D' A). apply eqv_sym. apply H. apply eqv_comm. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec