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