proposition: Lemma l10_4_spec : forall A B P P', ReflectL P P' A B -> ReflectL P' P A B.
proof: Proof. intros. unfold ReflectL in *. spliter. ex_and H X. split. exists X. split. apply l7_2. assumption. assumption. induction H0. left. apply perp_right_comm. assumption. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop