proposition: Lemma projp_idem : forall P P' A B, Projp P P' A B -> Projp P' P' A B.
proof: Proof. intros. unfold Projp in *. spliter. split. auto. induction H0. right. spliter. split. assumption. auto. right. spliter. subst P'. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors