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