proposition: Lemma diff_O_A : forall O E E' A mA, ~ Col O E E' -> Opp O E E' A mA -> Diff O E E' O A mA.
proof: Proof. intros. assert (Col O E A) by (unfold Opp, Sum, Ar2 in *; spliter; auto). assert (Col O E mA) by (unfold Opp, Sum, Ar2 in *; spliter; auto). revert H0; revert H1; revert H2; intros. unfold Diff. exists mA. split. assumption. apply sum_O_B; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg