proposition: Lemma le_zero : forall A B C, Le A B C C -> A=B.
proof: Proof. intros. assert (Le C C A B) by apply le_trivial. assert (Cong A B C C) by (apply le_anti_symmetry;assumption). treat_equalities;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col