proposition: Lemma bne_nat_ok : forall x y, bne_nat x y = true <-> x <> y.
proof: Proof. intros x y. unfold bne_nat. rewrite negb_lr. simpl. rewrite (beq_ko beq_nat_ok). refl. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)