proposition: Lemma smallest_comp m n : P m -> P n -> smallest m <= n.
proof: Proof. intros Pm Pn. destruct (le_dec m n). rewrite smallest_le_arg. hyp. rewrite smallest_inv with (n:=n); auto. apply smallest_le_arg. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)