fact: Definition lt_int (z z':Z) : bool := match z, z' with | Zpos n, Zpos m => lt_nat (nat_of_P n) (nat_of_P m) | Zpos n, _ => false | Z0, Zpos n => true | Z0, _ => false | Zneg n, Zneg m => lt_nat (nat_of_P m) (nat_of_P n) | Zneg n, _ => true end.
imports: CoRN.logic.CLogic Coq.Bool.Bool