proposition: Lemma l5_12_a : forall A B C, Bet A B C -> Le A B A C /\ Le B C A C.
proof: Proof. intros. split. unfold Le. exists B; split. assumption. apply cong_reflexivity. apply le_comm. unfold Le. exists B. split. apply between_symmetry. assumption. apply cong_reflexivity. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col