proposition: Lemma pi2mk n m: forall x y, pi2 (@mk n m x y) = y.
proof: Proof. intros [x Hx] [y Hy]. unfold pi2, mk. case eucl_dev. intros y' x' Hx' H. apply eq_ord. simpl. apply euclid_unique in H as [? _]; auto. nia. now apply ltb_lt. Qed.
imports: Psatz PeanoNat Compare_dec Euclid ordinal