proposition: Lemma diff_opp : forall O E E' A B AmB BmA, Diff O E E' A B AmB -> Diff O E E' B A BmA -> Opp O E E' AmB BmA.
proof: Proof. intros. assert(Ar2 O E E' A B AmB). apply diff_ar2; auto. assert(Ar2 O E E' B A BmA). apply diff_ar2; auto. unfold Ar2 in *. spliter. clean_duplicated_hyps. apply diff_sum in H. apply diff_sum in H0. induction(eq_dec_points A O). subst A. assert(BmA = B). apply(sum_O_B_eq O E E'); auto. subst BmA. unfold Opp. assumption. induction(eq_dec_points B O). subst B. assert(AmB = A). apply(sum_O_B_eq O E E'); auto. subst AmB. unfold Opp. apply sum_comm; auto. apply sum_cong in H0; auto. apply sum_cong in H; auto. assert(Parallelogram A O BmA B). apply plg_comm2. right. assumption. apply plg_permut in H4. apply plg_permut in H4. apply plg_permut in H4. assert(Parallelogram AmB O BmA O \/ AmB = O /\ B = A /\ O = BmA /\ AmB = O). apply(plg_pseudo_trans AmB O B A O BmA). apply plg_permut. apply plg_permut. apply plg_permut. right; assumption. assumption. assert(E <> O). intro. subst E. apply H1. Col. induction H9. induction H9. apply False_ind. unfold Parallelogram_strict in H9. unfold TS in H9. spliter. apply H13. ColR. unfold Parallelogram_flat in H. unfold Parallelogram_flat in H0. unfold Parallelogram_flat in H9. spliter. unfold Opp. apply cong_sum; Cong. right. intro. subst BmA. tauto. repeat split; Col. spliter. subst AmB. subst BmA. unfold Opp. apply sum_O_O; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg