proposition: Lemma bet_lt12_le13 : forall O E E' A B C, Bet A B C -> LtP O E E' A B -> LeP O E E' A C.
proof: Proof. intros O E E' A B C HBet HLt. apply leP_trans with B; [left; auto|]. apply bet_lt12_le23 with A; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod