fact: Fixpoint beq (x y : nat) := match x, y with | O, O => true | S x', S y' => beq x' y' | _, _ => false end.
imports: Coq.Arith.Arith Coq.micromega.Lia TLC(LibTactics LibReflect LibBool LibOperation LibRelation LibOrder)