proposition: Lemma opp_uniqueness : forall A MA1 MA2, Opp O E E' A MA1 -> Opp O E E' A MA2 -> MA1 = MA2.
proof: Proof. intros. unfold Opp in *. apply sum_comm in H. apply sum_comm in H0. induction(eq_dec_points A O). subst A. assert(HH:=sum_uniquenessB O MA1 MA2 O H H0). assumption. apply sum_plg in H. apply sum_plg in H0. ex_and H A'. ex_and H2 C'. ex_and H0 A''. ex_and H3 C''. apply plg_to_parallelogram in H. apply plg_to_parallelogram in H0. apply plg_to_parallelogram in H2. apply plg_to_parallelogram in H3. assert(Parallelogram C' A' A'' C'' \/ C' = A' /\ A = O /\ C'' = A'' /\ C' = C''). apply(plg_pseudo_trans C' A' A O C'' A''); auto. apply plg_permut. apply plg_permut. auto. induction H4. assert(Parallelogram O MA1 C'' A'' \/ O = MA1 /\ C' = A' /\ A'' = C'' /\ O = A''). apply(plg_pseudo_trans O MA1 C' A' A'' C''); auto. induction H5. assert(Parallelogram O MA1 MA2 O \/ O = MA1 /\ C'' = A'' /\ O = MA2 /\ O = O). apply(plg_pseudo_trans O MA1 C'' A'' O MA2); auto. apply plg_permut. apply plg_permut. assumption. induction H6. unfold Parallelogram in H6. induction H6. unfold Parallelogram_strict in H6. spliter. unfold TS in H6. spliter. apply False_ind. apply H9. Col. unfold Parallelogram_flat in H6. spliter. apply cong_symmetry in H9. apply cong_identity in H9. auto. spliter. subst MA1. subst MA2. auto. spliter. subst MA1. subst C''. subst A''. subst C'. unfold Parallelogram in H0. induction H0. unfold Parallelogram_strict in H0. spliter. apply par_distincts in H5. tauto. unfold Parallelogram_flat in H0. spliter. apply cong_identity in H6. auto. spliter. contradiction. left; auto. left; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg