proposition: Lemma bet_betCood : forall O E S U1 U2 A AX AY B BX BY C CX CY, Cd O E S U1 U2 A AX AY -> Cd O E S U1 U2 B BX BY -> Cd O E S U1 U2 C CX CY -> Bet A B C -> Bet AX BX CX /\ Bet AY BY CY.
proof: Proof. intros O E S U1 U2 A AX AY B BX BY C CX CY HCdA HCdB HCdC HBet. split; [apply bet_betCood_aux with O E S U1 U2 A AY B BY C CY|]; auto. apply bet_betCood_aux with O E S U2 U1 A AX B BX C CX; auto; apply coord_exchange_axes; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths