proposition: Lemma triangle_reverse_inequality : forall A B C D, Out A B D -> Cong A C A D -> Le B D B C.
proof: Proof. intros A B C D HABD HCong. elim(out_dec A B C); [|apply triangle_strict_reverse_inequality; auto]. intro. assert_diffs. assert(C = D) by (apply (l6_11_uniqueness A A C B); Cong; apply l6_6; auto). subst; Le. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2