proposition: Lemma inner_paschT : forall A B C P Q, BetG A P C -> BetG B Q C -> exists x, BetG P x B /\ BetG Q x A.
proof: Proof. intros A B C P Q HBet1 HBet2. elim (point_equality_decidabilityG A P); intro HDiff1; [rewrite HDiff1 in *; exists P; split; [apply bet_symmetryG|]; apply between_trivialT|]. elim (point_equality_decidabilityG P C); intro HDiff2; [rewrite HDiff2 in *; exists Q; split; apply bet_symmetryG; try apply between_trivialT; auto|]. elim (point_equality_decidabilityG B Q); intro HDiff3; [rewrite HDiff3 in *; exists Q; split; [|apply bet_symmetryG]; apply between_trivialT|]. elim (point_equality_decidabilityG Q C); intro HDiff4; [rewrite HDiff4 in *; exists P; split; apply bet_symmetryG; try apply between_trivialT; auto|]. elim (col_decG A B C); intro HCol; [|apply inner_paschG with C; auto]. do 2 (try (elim HCol; clear HCol; intro HCol)); rename HCol into HBet3. { exists B; split; [apply between_trivialT|]. apply bet_symmetryG; apply bet_inner_transitivityG with C; auto. } { exists C; split. { apply bet_symmetryG; apply bet_inner_transitivityG with A; auto; apply bet_symmetryG; auto. } { apply bet_symmetryG; apply bet_inner_transitivityG with B; apply bet_symmetryG; auto. } } { exists A; split; [|apply between_trivialT]. apply bet_symmetryG; apply bet_inner_transitivityG with C; auto; apply bet_symmetryG; auto. } Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le