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