proposition: Lemma project_par_eqv : forall P P' Q Q' A B X Y, Proj P P' A B X Y -> Proj Q Q' A B X Y -> Par P Q A B -> EqV P Q P' Q'.
proof: Proof. intros. assert(HH:=H). assert(HH0:=H0). unfold Proj in HH. unfold Proj in HH0. spliter. unfold EqV. apply par_distincts in H1. spliter. left. induction H1. induction H6; induction H11. assert(Par P P' Q Q'). eapply par_trans. apply H11. Par. assert(Par P' Q' A B ). right. repeat split; Col. intro. subst Q'. induction H14. apply H14. exists P'. split; Col. spliter. apply H1. exists P'. split; Col. clean_duplicated_hyps. assert(Par P Q P' Q'). eapply par_trans. left. apply H1. Par. assert(Par_strict P Q P' Q'). apply par_symmetry in H2. induction H2. apply par_strict_symmetry. assumption. spliter. apply False_ind. apply H1. exists P'. split; Col. apply plg_to_parallelogram. apply pars_par_plg; auto. apply par_strict_right_comm. assumption. subst P'. apply False_ind. apply H1. exists P. split; Col. subst Q'. apply False_ind. apply H1. exists Q. split; Col. subst P'. subst Q'. apply plg_trivial. assumption. spliter. assert(P = P' /\ Q = Q'). split; eapply (project_id A B X Y); Col. spliter. subst P'. subst Q'. apply plg_trivial. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors