proposition: Lemma is_image_rev : forall P P' A B, Reflect P P' A B -> Reflect P P' B A.
proof: Proof. intros. unfold Reflect in *. induction H. spliter. left. split. auto. apply is_image_spec_rev. assumption. right. spliter. subst. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop