n m : 0 < m -> (n | m) -> n <= m. Proof. intros H1 [x p]. destruct p, x. 1: contradiction (not_lt_zero_r _ H1). rapply (leq_mul_l _ _ 0). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes