proposition: Lemma halfa_not_null : forall P A O B, ~ Col A O B -> HalfA P A O B -> ~ Col A O P.
proof: Proof. intros P A O B HNCol [_ [HIn HConga]] HCol. assert (Col B O P). apply (col_conga_col A O P); assumption. apply HNCol. assert_diffs. ColR. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma