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