proposition: Lemma is_image_spec_rev : forall P P' A B, ReflectL P P' A B -> ReflectL P P' B A.
proof: Proof. unfold ReflectL. intros. spliter. split. ex_and H M0. exists M0. split. assumption. apply col_permutation_4. assumption. induction H0. left. apply perp_left_comm. assumption. right. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop