proposition: Lemma cong_le_le : forall A B C A' B' C', Bet A B C -> Bet A' B' C' -> Le B C B' C' -> Cong A B A' B' -> Le A C A' C'.
proof: Proof. intros. apply le_comm. eapply le_cong_le. apply between_symmetry. apply H. apply between_symmetry. apply H0. apply le_comm. assumption. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec