proposition: Lemma mkpi12 n m: forall p, @mk n m (pi1 p) (pi2 p) = p.
proof: Proof. intros [p Hp]. unfold pi1, pi2, mk. case eucl_dev. simpl. intros y x Hx Hy. apply eq_ord. simpl. now rewrite Hy. Qed.
imports: Psatz PeanoNat Compare_dec Euclid ordinal