IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerOrder

declarations in this module (443)

• theorem le_refl L28
• theorem le_trans L31
• theorem le_antisymm_balanced L37
• theorem le_total L44
• theorem trichotomy L49
• theorem negativeFlag_eq_true_iff_nonnegFlag_eq_false L59
• theorem negativeFlag_eq_false_iff_nonnegFlag_eq_true L64
• theorem signFlags_exclusive L69
• theorem signFlags_exhaustive L77
• theorem zero_le_iff_nonnegFlag L86
• theorem lt_zero_iff_negativeFlag L91
• theorem zero_lt_iff_nonnegFlag_and_not_balanced_zero L96
• theorem nonnegFlag_eq_of_balanced L108
• theorem negativeFlag_eq_of_balanced L126
• theorem nonneg_iff_of_balanced L132
• theorem add_congr_of_balanced L145
• theorem negate_congr_of_balanced L151
• theorem sub_congr_of_balanced L157
• theorem sub_congr_of_balanced_left L164
• theorem sub_congr_of_balanced_right L171
• theorem nonnegFlag_sub_eq_of_balanced_left L178
• theorem nonnegFlag_sub_eq_of_balanced_right L185
• theorem negativeFlag_sub_eq_of_balanced_left L192
• theorem negativeFlag_sub_eq_of_balanced_right L199
• theorem nonnegFlag_sub_eq_of_balanced L206
• theorem negativeFlag_sub_eq_of_balanced L213
• theorem scaleByNat_congr_of_balanced L220
• theorem scaleByNat_balanced_zero_of_balanced_zero L226
• theorem mul_ofOrbit_balanced_scaleByNat L233
• theorem ofOrbit_mul_balanced_scaleByNat L241
• theorem abs_mul L250
• theorem mul_balanced_zero_iff L256
• theorem mul_not_balanced_zero_iff L276
• theorem balanced_mul_left_iff_of_not_balanced_zero L294
• theorem balanced_mul_right_iff_of_not_balanced_zero L312
• theorem le_mul_left_iff_of_nonnegFlag_of_not_balanced_zero L330
• theorem lt_mul_left_iff_of_nonnegFlag_of_not_balanced_zero L348
• theorem le_mul_right_iff_of_nonnegFlag_of_not_balanced_zero L366
• theorem lt_mul_right_iff_of_nonnegFlag_of_not_balanced_zero L384
• theorem le_mul_left_iff_of_negativeFlag L402
• theorem lt_mul_left_iff_of_negativeFlag L413
• theorem le_mul_right_iff_of_negativeFlag L424
• theorem lt_mul_right_iff_of_negativeFlag L435
• theorem abs_mul_eq_zero_iff L446
• theorem abs_mul_ne_zero_iff L465
• theorem abs_mul_eq_zero_iff_balanced_zero L482
• theorem abs_mul_ne_zero_iff_not_balanced_zero L502
• theorem abs_scaleByNat L520
• theorem abs_mul_ofOrbit_right L527
• theorem abs_mul_ofOrbit_left L534
• theorem mul_ofOrbit_right_balanced_zero_iff L542
• theorem mul_ofOrbit_left_balanced_zero_iff L567
• theorem mul_ofOrbit_right_not_balanced_zero_iff L592
• theorem mul_ofOrbit_left_not_balanced_zero_iff L610
• theorem nonnegFlag_scaleByNat_of_ne_zero L628
• theorem negativeFlag_scaleByNat_of_ne_zero L652
• theorem scaleByNat_balanced_zero_iff L658
• theorem scaleByNat_not_balanced_zero_iff L682
• theorem abs_scaleByNat_eq_zero_iff L699
• theorem abs_scaleByNat_ne_zero_iff L720
• theorem abs_mul_ofOrbit_right_eq_zero_iff L737
• theorem abs_mul_ofOrbit_left_eq_zero_iff L758
• theorem abs_mul_ofOrbit_right_ne_zero_iff L779
• theorem abs_mul_ofOrbit_left_ne_zero_iff L796
• theorem le_scaleByNat_of_le L813
• theorem le_scaleByNat_iff_of_ne_zero L821
• theorem lt_scaleByNat_iff_of_ne_zero L837
• theorem balanced_scaleByNat_iff_of_ne_zero L853
• theorem le_congr_left_of_balanced L869
• theorem le_congr_right_of_balanced L875
• theorem lt_congr_left_of_balanced L881
• theorem lt_congr_right_of_balanced L887
• theorem le_congr_of_balanced L893
• theorem lt_congr_of_balanced L899
• def cmp L907
• theorem cmp_eq_lt_of_lt L915
• theorem cmp_eq_eq_of_balanced L927
• theorem cmp_eq_gt_of_gt L932
• theorem cmp_eq_lt_iff L944
• theorem cmp_eq_eq_iff L960

… and 363 more