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