proposition: Lemma ker_col : forall P Q P' A B X Y, Proj P P' A B X Y -> Proj Q P' A B X Y -> Col P Q P'.
proof: Proof. intros. unfold Proj in *. spliter. clean_duplicated_hyps. induction H8; induction H4; try(subst P';Col). assert(Par P P' Q P'). eapply par_trans. apply H0. Par. induction H2. apply False_ind. apply H2. exists P'; Col. spliter. Col. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors