proposition: Lemma bgt_nat_ok : forall x y, bgt_nat x y = true <-> x > y.
proof: Proof. induction x; destruct y; simpl; split; intro; try (lia||discr||refl). rewrite IHx in H. lia. rewrite IHx. lia. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)