proposition: Lemma diff_O_A_opp : forall O E E' A mA, Diff O E E' O A mA -> Opp O E E' A mA.
proof: Proof. intros. assert(Ar2 O E E' O A mA). apply diff_ar2;auto. unfold Diff in H. ex_and H A'. assert(Ar2 O E E' O A' mA). apply sum_ar2; auto. unfold Ar2 in *. spliter. clean_duplicated_hyps. assert(Sum O E E' O A' A'). apply (sum_O_B); auto. assert(mA = A'). apply(sum_uniqueness O E E' O A'); auto. subst A'. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg