proposition: Lemma diff_ar2 : forall O E E' A B AMB, Diff O E E' A B AMB -> Ar2 O E E' A B AMB.
proof: Proof. intros. unfold Diff in H. ex_and H MA. unfold Opp in H. unfold Sum in *. spliter. unfold Ar2 in *. spliter. repeat split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg