proposition: Lemma eq_le2__eq2 : forall p1 p2 p3 p4, Pos.le p1 p2 -> Pos.le p3 p4 -> (Pos.eq (fstpp (p1, p2)) (fstpp (p3, p4)) /\ Pos.eq (sndpp (p1, p2)) (sndpp (p3, p4))) -> (p1 = p3 /\ p2 = p4).
proof: Proof. intros p1 p2 p3 p4 Hle Hle'. unfold fstpp, sndpp, Pos.eq. rewrite 2 Pos.min_l; [rewrite 2 Pos.max_r|..]; trivial. Qed.
imports: Recdef NArith GeoCoq.Utils.sets