fact: Fixpoint bgt_nat (x y : nat) := match x, y with | 0, _ => false | S _, 0 => true | S x', S y' => bgt_nat x' y' end.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)