proposition: Lemma l11_44_2bis : forall A B C, ~ Col A B C -> (LeA B A C B C A <-> Le B C B A).
proof: Proof. intros; split; intro. apply nlt__le. intro. apply (lea__nlta B A C B C A). assumption. apply l11_44_2; Col. induction (cong_dec B C B A). apply conga__lea. apply l11_44_1; Cong. apply lta__lea. apply l11_44_2. assumption. split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2