proposition: Lemma t22_9__per : forall N M P Q R S, Lambert N M P Q -> Lambert N M R S -> Bet M P R -> Bet N Q S -> (Per S R M <-> Per Q P M).
proof: Proof. intros N M P Q R S HLamP HLamR HR HS. apply (t22_9_aux N); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma