fact: Definition i63ltb (x y : i63) : bool := let max_int := un_i63 max_i63 in let x := un_i63 x in let y := un_i63 y in if ((ltb x max_int) && (ltb y max_int)) || ((ltb max_int x)%int63 && (ltb max_int y)) then (ltb x y)%int63 else if (ltb max_int x)%int63 then true else false.
imports: Coq(NArith ZArith Int63 Program.Wf)