proposition: Lemma eq_pseudo_refl : forall p q, Pos.eq (fstpp (p, q)) (fstpp (q, p)) /\ Pos.eq (sndpp (p, q)) (sndpp (q, p)).
proof: Proof. cut (forall p q, Pos.le p q -> Pos.eq (fstpp (p, q)) (fstpp (q, p)) /\ Pos.eq (sndpp (p, q)) (sndpp (q, p))). intros Haux p q. case_eq (Pos.leb p q); intro Hpq. apply Haux, Pos.leb_le, Hpq. apply SP.Raw.MX.eq_sym, Haux, Pos.lt_le_incl, Pos.leb_gt, Hpq. intros p q Hle. unfold fstpp, sndpp. rewrite Pos.min_l; trivial. rewrite Pos.min_r; trivial. rewrite Pos.max_r; trivial. rewrite Pos.max_l; trivial. split; reflexivity. Qed.
imports: Recdef NArith GeoCoq.Utils.sets