proposition: Lemma beq_nat_ok : forall x y, beq_nat x y = true <-> x = y.
proof: Proof. induction x; destruct y; simpl; split; intro; try (refl || discr). f_equal. fo. fo. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)