proposition: Lemma ker_par : forall P Q P' A B X Y, P <> Q -> Proj P P' A B X Y -> Proj Q P' A B X Y -> Par P Q X Y.
proof: Proof. intros. assert(Col P Q P'). eapply ker_col. apply H0. apply H1. unfold Proj in *. spliter. clean_duplicated_hyps. induction H10; induction H6. eapply (par_col_par_2 _ P'). assumption. Col. assumption. subst P'. assumption. subst P'. Par. subst P'. apply False_ind. apply H. auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors