Library Numbers
Require Export ZArith.
Module Type Num.
Parameter A:Type.
Parameter a0:A.
Parameter a1:A.
Parameter plusA : A → A → A.
Parameter multA : A → A → A.
Parameter oppA : A → A.
Parameter divA : A → A → A.
Parameter modA : A → A → A.
Parameter absA : A→ A.
Parameter equalA : A → A → Prop.
Parameter leA : A → A → Prop.
Parameter ltA : A → A → Prop.
Notation " x == y" := (equalA x y) (at level 80).
Notation "x + y " := (plusA x y).
Notation "x * y " := (multA x y).
Notation "x / y " := (divA x y).
Notation "x %% y" := (modA x y) (at level 100).
Notation "0" := (a0).
Notation "1" := (a1).
Notation "- x" := (oppA x).
Notation "| x |" := (absA x) (at level 60).
Notation "x <= y" := (leA x y).
Notation "x < y" := (ltA x y).
Parameter equalA_refl : ∀ x, x == x.
Parameter equalA_sym : ∀ x y, x == y → y ==x.
Parameter equalA_trans : ∀ x y z, x == y → y ==z → x==z.
Parameter plus_neutral : ∀ x,0 + x == x.
Parameter plus_comm : ∀ x y, x + y == y + x.
Parameter plus_assoc : ∀ x y z, x + (y + z) == (x + y) + z.
Parameter plus_opp : ∀ x, x + (- x) == 0.
Parameter abs_pos : ∀ x, 0 ≤|x|.
Parameter abs_pos_val : ∀ x, 0 ≤x → |x|==x.
Parameter abs_neg_val : ∀ x, x ≤0 → |x|==-x.
Parameter abs_minus : ∀ x, | - x| == |x|.
Parameter abs_max : ∀ x, x ≤ |x|.
Parameter abs_new : ∀ x a, x≤ a → -x ≤a → |x|≤a.
Parameter abs_new2 : ∀ x a, |x|≤ a → -a ≤ x .
Parameter abs_triang : ∀ x y, |x+y| ≤ |x| + | y |.
Parameter abs_prod : ∀ x y, |x × y| == |x| × |y|.
Parameter div_mod : ∀ a b, 0< a∨a< 0 → b == a*(b / a) + (b %% a).
Parameter div_mod2 : ∀ a b, 0< a∨a< 0 → a*(b/a) == b + - (b %% a).
Parameter div_mod3 : ∀ a b, 0 < a → |(b %% a)| < a.
Parameter div_mod3a : ∀ a b, 0 < a → (b %% a) < a.
Parameter div_mod3b : ∀ a b, 0 < a → 0<=(b %% a).
Parameter div_mod3_abs: ∀ a b:A, 0< b ∨ b< 0 → | a %% b | ≤ |b|.
Parameter div_le : ∀ a b c, 0 < c → a ≤ b → a / c ≤ b / c.
Parameter div_le2 : ∀ a b, 0 < a → 0≤ b → a*(b/a) ≤ b.
Parameter div_pos : ∀ a b, 0≤a → 0<b → 0≤a/b.
Parameter div_idg : ∀ x y, 0 < y → (x × y) / y == x.
Parameter mult_le : ∀ a b c d,
0 ≤ a → a ≤ b → 0 ≤ c → c ≤ d → a×c ≤ b × d.
Parameter mult_neutral : ∀ x, 1 × x == x.
Parameter mult_distr_l : ∀ x y z, (x+y)*z == x×z + y×z.
Parameter mult_comm : ∀ x y, x × y == y × x.
Parameter mult_assoc : ∀ x y z, x × (y × z) ==(x × y) × z.
Parameter mult_absorb : ∀ x, x × 0 == 0.
Parameter le_refl : ∀ x, x ≤ x.
Parameter le_trans : ∀ x y z, x ≤ y → y ≤ z → x ≤ z .
Parameter lt_plus : ∀ x y z t, x < y → z < t → (x + z) < (y + t).
Parameter le_plus : ∀ x y z t, x ≤ y → z ≤ t → (x + z) ≤ (y + t).
Parameter le_lt_plus : ∀ x y z t, x ≤ y → z < t → (x + z) < (y + t).
Parameter le_plus_inv : ∀ x y z, (x + z) ≤ (y + z) → x ≤ y .
Parameter lt_plus_inv : ∀ x y z, (x + z) < (y + z) → x < y .
Parameter le_mult_simpl : ∀ x y z , (0 ≤ z) → (x ≤y)-> (x × z) ≤ (y ×z).
Parameter le_mult : ∀ x y z, 0 ≤ x → y ≤z → x×y ≤ x×z.
Parameter le_mult_general :
∀ x y z t, 0 ≤ x → x ≤ y → 0 ≤ z → z ≤ t → x×z ≤ y×t.
Parameter le_mult_neg : ∀ x y z, x < 0 → y ≤z → x×z ≤ x×y.
Parameter le_mult_inv : ∀ x y z, 0 < x → (x × y) ≤ (x × z) → y ≤ z .
Parameter lt_mult_inv : ∀ x y z, 0 < x → (x × y) < (x × z) → y < z .
Parameter le_mult_inv2 : ∀ x y z, x < 0 → (x × y) ≤ (x × z) → z ≤ y .
Parameter lt_mult_inv2 : ∀ x y z, x < 0 → (x × y) < (x × z) → z < y .
Parameter lt_mult : ∀ x y z, 0 < x → y <z → x×y < x×z.
Parameter mult_pos : ∀ x y : A, 0<x → 0<y → 0<x×y.
Parameter lt_0_1 : (0 < 1).
Parameter lt_m1_0 : (-a1 < 0).
Parameter lt_trans : ∀ x y z, x < y → y < z → x < z .
Parameter le_lt_trans : ∀ x y z, x ≤ y → y < z → x < z .
Parameter lt_le_trans : ∀ x y z, x < y → y ≤ z → x < z .
Parameter lt_le : ∀ x y, (x < y) → (x ≤ y).
Parameter lt_le_2 : ∀ x y, (x < y) → (x+1 ≤ y). Parameter le_lt_False : ∀ x y, x ≤ y → y < x → False.
Parameter le_id : ∀ x y, x ≤ y → y ≤ x → x == y.
Parameter contradict_lt_le : ∀ s x, s < x → x ≤ s → False.
Parameter not_lt_0_0 : ¬0 < 0.
Parameter lim:A→Prop.
Parameter ANS1 : lim 1.
Parameter ANS2a : ∀ x y, lim x → lim y → lim (x + y).
Parameter ANS2b : ∀ x y, lim x → lim y → lim (x × y).
Parameter ANS4 : ∀ x, (∃ y, lim y∧ | x | ≤ | y |)-> lim x.
End Num.
Module Type Num.
Parameter A:Type.
Parameter a0:A.
Parameter a1:A.
Parameter plusA : A → A → A.
Parameter multA : A → A → A.
Parameter oppA : A → A.
Parameter divA : A → A → A.
Parameter modA : A → A → A.
Parameter absA : A→ A.
Parameter equalA : A → A → Prop.
Parameter leA : A → A → Prop.
Parameter ltA : A → A → Prop.
Notation " x == y" := (equalA x y) (at level 80).
Notation "x + y " := (plusA x y).
Notation "x * y " := (multA x y).
Notation "x / y " := (divA x y).
Notation "x %% y" := (modA x y) (at level 100).
Notation "0" := (a0).
Notation "1" := (a1).
Notation "- x" := (oppA x).
Notation "| x |" := (absA x) (at level 60).
Notation "x <= y" := (leA x y).
Notation "x < y" := (ltA x y).
Parameter equalA_refl : ∀ x, x == x.
Parameter equalA_sym : ∀ x y, x == y → y ==x.
Parameter equalA_trans : ∀ x y z, x == y → y ==z → x==z.
Parameter plus_neutral : ∀ x,0 + x == x.
Parameter plus_comm : ∀ x y, x + y == y + x.
Parameter plus_assoc : ∀ x y z, x + (y + z) == (x + y) + z.
Parameter plus_opp : ∀ x, x + (- x) == 0.
Parameter abs_pos : ∀ x, 0 ≤|x|.
Parameter abs_pos_val : ∀ x, 0 ≤x → |x|==x.
Parameter abs_neg_val : ∀ x, x ≤0 → |x|==-x.
Parameter abs_minus : ∀ x, | - x| == |x|.
Parameter abs_max : ∀ x, x ≤ |x|.
Parameter abs_new : ∀ x a, x≤ a → -x ≤a → |x|≤a.
Parameter abs_new2 : ∀ x a, |x|≤ a → -a ≤ x .
Parameter abs_triang : ∀ x y, |x+y| ≤ |x| + | y |.
Parameter abs_prod : ∀ x y, |x × y| == |x| × |y|.
Parameter div_mod : ∀ a b, 0< a∨a< 0 → b == a*(b / a) + (b %% a).
Parameter div_mod2 : ∀ a b, 0< a∨a< 0 → a*(b/a) == b + - (b %% a).
Parameter div_mod3 : ∀ a b, 0 < a → |(b %% a)| < a.
Parameter div_mod3a : ∀ a b, 0 < a → (b %% a) < a.
Parameter div_mod3b : ∀ a b, 0 < a → 0<=(b %% a).
Parameter div_mod3_abs: ∀ a b:A, 0< b ∨ b< 0 → | a %% b | ≤ |b|.
Parameter div_le : ∀ a b c, 0 < c → a ≤ b → a / c ≤ b / c.
Parameter div_le2 : ∀ a b, 0 < a → 0≤ b → a*(b/a) ≤ b.
Parameter div_pos : ∀ a b, 0≤a → 0<b → 0≤a/b.
Parameter div_idg : ∀ x y, 0 < y → (x × y) / y == x.
Parameter mult_le : ∀ a b c d,
0 ≤ a → a ≤ b → 0 ≤ c → c ≤ d → a×c ≤ b × d.
Parameter mult_neutral : ∀ x, 1 × x == x.
Parameter mult_distr_l : ∀ x y z, (x+y)*z == x×z + y×z.
Parameter mult_comm : ∀ x y, x × y == y × x.
Parameter mult_assoc : ∀ x y z, x × (y × z) ==(x × y) × z.
Parameter mult_absorb : ∀ x, x × 0 == 0.
Parameter le_refl : ∀ x, x ≤ x.
Parameter le_trans : ∀ x y z, x ≤ y → y ≤ z → x ≤ z .
Parameter lt_plus : ∀ x y z t, x < y → z < t → (x + z) < (y + t).
Parameter le_plus : ∀ x y z t, x ≤ y → z ≤ t → (x + z) ≤ (y + t).
Parameter le_lt_plus : ∀ x y z t, x ≤ y → z < t → (x + z) < (y + t).
Parameter le_plus_inv : ∀ x y z, (x + z) ≤ (y + z) → x ≤ y .
Parameter lt_plus_inv : ∀ x y z, (x + z) < (y + z) → x < y .
Parameter le_mult_simpl : ∀ x y z , (0 ≤ z) → (x ≤y)-> (x × z) ≤ (y ×z).
Parameter le_mult : ∀ x y z, 0 ≤ x → y ≤z → x×y ≤ x×z.
Parameter le_mult_general :
∀ x y z t, 0 ≤ x → x ≤ y → 0 ≤ z → z ≤ t → x×z ≤ y×t.
Parameter le_mult_neg : ∀ x y z, x < 0 → y ≤z → x×z ≤ x×y.
Parameter le_mult_inv : ∀ x y z, 0 < x → (x × y) ≤ (x × z) → y ≤ z .
Parameter lt_mult_inv : ∀ x y z, 0 < x → (x × y) < (x × z) → y < z .
Parameter le_mult_inv2 : ∀ x y z, x < 0 → (x × y) ≤ (x × z) → z ≤ y .
Parameter lt_mult_inv2 : ∀ x y z, x < 0 → (x × y) < (x × z) → z < y .
Parameter lt_mult : ∀ x y z, 0 < x → y <z → x×y < x×z.
Parameter mult_pos : ∀ x y : A, 0<x → 0<y → 0<x×y.
Parameter lt_0_1 : (0 < 1).
Parameter lt_m1_0 : (-a1 < 0).
Parameter lt_trans : ∀ x y z, x < y → y < z → x < z .
Parameter le_lt_trans : ∀ x y z, x ≤ y → y < z → x < z .
Parameter lt_le_trans : ∀ x y z, x < y → y ≤ z → x < z .
Parameter lt_le : ∀ x y, (x < y) → (x ≤ y).
Parameter lt_le_2 : ∀ x y, (x < y) → (x+1 ≤ y). Parameter le_lt_False : ∀ x y, x ≤ y → y < x → False.
Parameter le_id : ∀ x y, x ≤ y → y ≤ x → x == y.
Parameter contradict_lt_le : ∀ s x, s < x → x ≤ s → False.
Parameter not_lt_0_0 : ¬0 < 0.
Parameter lim:A→Prop.
Parameter ANS1 : lim 1.
Parameter ANS2a : ∀ x y, lim x → lim y → lim (x + y).
Parameter ANS2b : ∀ x y, lim x → lim y → lim (x × y).
Parameter ANS4 : ∀ x, (∃ y, lim y∧ | x | ≤ | y |)-> lim x.
End Num.