proposition: Lemma l11_44_1_b : forall A B C, ~ Col A B C -> CongA B A C B C A -> Cong B A B C.
proof: Proof. intros. apply not_col_distincts in H. spliter. assert(HH:= or_lt_cong_gt B A B C). induction HH. apply l11_44_2_a in H4. apply lta_not_conga in H4. apply conga_sym in H0. contradiction. assumption. induction H4. unfold Gt in H4. apply l11_44_2_a in H4. apply lta_not_conga in H4. contradiction. intro. apply H. apply col_permutation_3. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2