proposition: Lemma cong_le_per2__le : forall A B C A' B' C', Per A B C -> Per A' B' C' -> Cong A B A' B' -> Le B C B' C' -> Le A C A' C'.
proof: Proof. intros. destruct (cong_dec B C B' C'). apply cong__le, l10_12 with B B'; assumption. assert (Lt B C B' C') by (split; assumption). apply lt__le, cong_lt_per2__lt with B B'; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2