proposition: Lemma l11_44_2_b : forall A B C, LtA B A C B C A -> Lt B C B A.
proof: Proof. intros. induction (col_dec A B C). assert (Hd := H). apply lta_distincts in Hd; spliter; clean_reap_hyps. apply col_lta__bet in H; Col; Le. apply not_col_distincts in H0. spliter. assert(HH:= or_lt_cong_gt B A B C). induction HH. apply l11_44_2_a in H4. assert(HH:= not_and_lta B A C B C A). exfalso. apply HH. split; assumption. assumption. induction H4. unfold Gt in H4. assumption. apply l11_44_1_a in H4; auto. apply lta_not_conga in H; auto. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2