proposition: Lemma lt_diff_ps : forall O E E' X Y XMY, Col O E X -> Col O E Y -> LtP O E E' Y X -> Diff O E E' X Y XMY -> Ps O E XMY.
proof: Proof. intros O E E' X Y XMY HCol1 HCol2 HLt HXMY. destruct HLt as [XMY' [HDiff HPs]]. apply (diff_uniqueness _ _ _ _ _ XMY) in HDiff; treat_equalities; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod