Std.Proof.IntDiscrete
View source →Discreteness of the inductive integers: strict comparison against right
is the same Boolean proposition as non-strict comparison against right-1.
Functions
-
# fn lt_int_is_le_predecessor(left: Int, right: Int) -> Equivalent(Bool, lt_int(left, right), le_int(left, pred_int(right)))
-
# fn lt_nat_is_le_successor_left(left: Nat, right: Nat) -> Equivalent(Bool, lt_nat(left, right), le_nat(S(left), right))
-
# fn lt_nat_successor_right_is_le(left: Nat, right: Nat) -> Equivalent(Bool, lt_nat(left, S(right)), le_nat(left, right))