proposition: Lemma ltb_lt x y: ltb x y = true <-> lt x y.
proof: Proof. revert y. induction x; destruct y; simpl. split. discriminate. inversion 1. split. lia. trivial. split. discriminate. inversion 1. rewrite IHx. lia. Qed.
imports: Psatz PeanoNat Compare_dec Euclid ordinal