proposition: Lemma opp0_uniqueness : forall M, Opp O E E' O M -> M = O.
proof: Proof. intros. assert(NC:= grid_ok). unfold Opp in H. apply sum_to_sump in H. unfold Sump in H. spliter. ex_and H1 A'. ex_and H2 C'. ex_and H1 P'. unfold Proj in *. spliter. induction H8. induction H12. assert(Par O E' E E'). apply (par_trans _ _ C' O). apply par_symmetry. Par. Par. apply False_ind. induction H17. apply H17. exists E'. split; Col. spliter. contradiction. subst C'. apply par_distincts in H8. tauto. subst C'. assert( A' = O). apply (l6_21 O E E' O); Col. induction H2. apply False_ind. apply H2. exists O. split; Col. spliter. apply col_permutation_1. apply(col_transitivity_1 _ P'); Col. subst A'. induction H16. induction H8. apply False_ind. apply H8. exists E. split; Col. spliter. contradiction. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg