Thm* a,b: , e:({a..b }  ). b a  ( i:{a..b }. e(i)) = 0 | [sum_via_intseg_null] |
Thm* a,b: , e:({a..b }  ). b a  ( i:{a..b }. e(i)) = 1 | [mul_via_intseg_null] |
Thm* m,k: . m k  k!m = ((k!) ((k-m)!)) | [factorial_ratio2] |
Thm* m,k: . m k  k! = (k-m)! k!m | [factorial_ratio] |
Thm* m,k: . 1 m k  k!m = k (k-1)!(m-1)  | [factorial_tail_via_iter_step_rw] |
Thm* m,k: . 1 m k  ( k',m': . k' = k-1  m' = m-1  k!m = k k'!m' ) | [factorial_tail_via_iter_step] |
Thm* m,k: . k<m  k!m = 0  | [factorial_tail_via_iter_zero] |
Thm* m,k: . m = 0  k!m = 1  | [factorial_tail_via_iter_null] |
Thm* n,m,k: . n k-m  m k  k!(n+m) = (k-m)!n k!m | [factorial_tail_split_mid] |
Thm* ( i:{a..b }. e(i) = 0)  ( i:{a..b }. e(i)) = 0 | [zero_ann_iter_via_intseg] |
Thm* a,b: , P:({a..b } Prop). b a  ( i:{a..b }. P(i)) | [exist_intseg_null] |
Thm* a,b: , P:({a..b } Prop).
Thm* a<b  (( i:{a..b }. P(i))  ( i:{a..(b-1) }. P(i)) P(b-1)) | [or_via_exist_intseg_split_last] |
Thm* a,b: , P:({a..b } Prop).
Thm* a<b
Thm* 
Thm* ( c: . b = c+1  (( i:{a..b }. P(i))  ( i:{a..c }. P(i)) P(c))) | [or_via_exist_intseg_notnull] |
Thm* a,b: , P:({a..b } Prop).
Thm* a<b  (( i:{a..b }. P(i))  ( i:{a..(b-1) }. P(i)) & P(b-1)) | [and_via_all_intseg_split_last] |
Thm* a,b: , P:({a..b } Prop).
Thm* a<b
Thm* 
Thm* ( c: . b = c+1  (( i:{a..b }. P(i))  ( i:{a..c }. P(i)) & P(c))) | [and_via_all_intseg_notnull] |
Thm* a,b: , e:({a..b }  ).
Thm* a<b  ( i:{a..b }. e(i)) = ( i:{a..b-1 }. e(i))+e(b-1) | [sum_via_intseg_split_last] |
Thm* a,b: , e:({a..b }  ).
Thm* a<b  ( i:{a..b }. e(i)) = ( i:{a..b-1 }. e(i)) e(b-1) | [mul_via_intseg_split_last] |
Thm* a,c,b: , e:({a..b }  ).
Thm* a c
Thm* 
Thm* c b  ( i:{a..b }. e(i)) = ( i:{a..c }. e(i)) ( i:{c..b }. e(i)) | [mul_via_intseg_split_mid] |
Thm* a,c,b: , e:({a..b }  ).
Thm* a c
Thm* 
Thm* c b  ( i:{a..b }. e(i)) = ( i:{a..c }. e(i))+( i:{c..b }. e(i)) | [sum_via_intseg_split_mid] |
Thm* a,c,b: , e:({a..b }  ).
Thm* a c
Thm* 
Thm* c<b
Thm* 
Thm* ( i:{a..b }. e(i)) = ( i:{a..c }. e(i)) e(c) ( i:{c+1..b }. e(i)) | [mul_via_intseg_split_pluck] |
Thm* a,c,b: , e:({a..b }  ).
Thm* a c
Thm* 
Thm* c<b
Thm* 
Thm* ( i:{a..b }. e(i)) = ( i:{a..c }. e(i))+e(c)+( i:{c+1..b }. e(i)) | [sum_via_intseg_split_pluck] |
Thm* f:(A A A), u:A.
Thm* is_ident(A; f; u)
Thm* 
Thm* is_assoc_sep(A; f)
Thm* 
Thm* ( a,c,b: , e:({a..b } A).
Thm* (a c
Thm* (
Thm* (c<b
Thm* (
Thm* ((Iter(f;u) i:{a..b }. e(i))
Thm* (=
Thm* (f((Iter(f;u) i:{a..c }. e(i)),f(e(c),Iter(f;u) i:{c+1..b }. e(i)))) | [iter_via_intseg_split_pluck] |
Thm* f:(A A A), u:A.
Thm* is_ident(A; f; u)
Thm* 
Thm* is_assoc_sep(A; f)
Thm* 
Thm* ( a,b: , c:{a...b}, d:{c..b }, e:({a..b } A).
Thm* (( i:{a..b }. i<c d i  e(i) = u)
Thm* (
Thm* ((Iter(f;u) i:{a..b }. e(i)) = (Iter(f;u) i:{c..d }. e(i))) | [iter_via_intseg_amputate_units] |
Thm* f:(A A A), u:A.
Thm* is_ident(A; f; u)
Thm* 
Thm* is_assoc_sep(A; f)
Thm* 
Thm* ( a,c,b: , e:({a..b } A).
Thm* (a c
Thm* (
Thm* (c b
Thm* (
Thm* ((Iter(f;u) i:{a..b }. e(i))
Thm* (=
Thm* (f((Iter(f;u) i:{a..c }. e(i)),Iter(f;u) i:{c..b }. e(i))) | [iter_via_intseg_split_mid] |
Thm* f:(A A A), u:A.
Thm* is_commutative_sep(A; f)
Thm* 
Thm* is_ident(A; f; u)
Thm* 
Thm* is_assoc_sep(A; f)
Thm* 
Thm* ( a,b: , e,g:({a..b } A).
Thm* (f((Iter(f;u) i:{a..b }. e(i)),Iter(f;u) i:{a..b }. g(i))
Thm* (=
Thm* ((Iter(f;u) i:{a..b }. f(e(i),g(i)))
Thm* ( A) | [iter_via_intseg_comp_binop] |
Thm* f:(A A A), u:A, a,b,c,d: .
Thm* b-a = d-c
Thm* 
Thm* ( e:({a..b } A), g:({c..d } A).
Thm* (( i:{a..b }, j:{c..d }. j-i = c-a  e(i) = g(j) A)
Thm* (
Thm* ((Iter(f;u) i:{a..b }. e(i)) = (Iter(f;u) j:{c..d }. g(j))) | [iter_via_intseg_shift] |
Thm* a,b: , e:({a..b }  ). ( i:{a..b }. e(i) = 1)  ( i:{a..b }. e(i)) = 1 | [mul_via_intseg_one] |
Thm* f:(A A A), u:A.
Thm* is_ident(A; f; u)
Thm* 
Thm* ( a,b: , e:({a..b } A).
Thm* (( i:{a..b }. e(i) = u)  (Iter(f;u) i:{a..b }. e(i)) = u) | [iter_via_intseg_all_units] |
Thm* f:(A A A), u:A, a,b: , e:({a..b } A).
Thm* a<b
Thm* 
Thm* (Iter(f;u) i:{a..b }. e(i)) = f((Iter(f;u) i:{a..b-1 }. e(i)),e(b-1)) | [iter_via_intseg_split_last] |
Thm* a,b: , e:({a..b }  ).
Thm* a<b  ( c: . b = c+1  ( i:{a..b }. e(i)) = ( i:{a..c }. e(i))+e(c)) | [sum_via_intseg_notnull] |
Thm* a,b: , e:({a..b }  ).
Thm* a<b  ( c: . b = c+1  ( i:{a..b }. e(i)) = ( i:{a..c }. e(i)) e(c)) | [mul_via_intseg_notnull] |
Thm* f:(A A A), u:A, a,b: , e:({a..b } A).
Thm* a<b
Thm* 
Thm* ( c: .
Thm* (b = c+1
Thm* (
Thm* ((Iter(f;u) i:{a..b }. e(i)) = f((Iter(f;u) i:{a..c }. e(i)),e(c))) | [iter_via_intseg_notnull] |
Thm* a,b: , e:({a..b }  ). a+1 = b  ( i:{a..b }. e(i)) = e(a) | [mul_via_intseg_singleton] |
Thm* a,b: , e:({a..b }  ). a+1 = b  ( i:{a..b }. e(i)) = e(a) | [sum_via_intseg_singleton] |
Thm* f:(A A A), u:A.
Thm* is_ident(A; f; u)
Thm* 
Thm* ( a,b: , e:({a..b } A). a+1 = b  (Iter(f;u) i:{a..b }. e(i)) = e(a)) | [iter_via_intseg_singleton] |
Thm* f:(A A A), u:A, a,b: , e:({a..b } A).
Thm* b a  (Iter(f;u) i:{a..b }. e(i)) = (Iter(f;u) i:{a..a }. e(i)) | [iter_via_intseg_nullnorm] |
Thm* f:(A A A), u:A, a,b: , e:({a..b } A).
Thm* b a  (Iter(f;u) i:{a..b }. e(i)) = u | [iter_via_intseg_null] |
Thm* P:(     Prop).
Thm* ( a: , b:{...a}. P(a,b))
Thm* 
Thm* ( a: , b:{a+1...}. ( c:{a..b }. P(a,c))  P(a,b))  ( a,b: . P(a,b)) | [all_int_segs_by_upper_ind] |
Thm* P:(     Prop), a: .
Thm* ( b:{...a}. P(a,b))
Thm* 
Thm* ( b:{a+1...}. ( c:{a..b }. P(a,c))  P(a,b))  ( b: . P(a,b)) | [int_segs_from_base_by_upper_ind] |
Thm* P:(     Prop), a: .
Thm* ( b:{...a}. P(a,a)  P(a,b))  ( b:{a...}. P(a,b))  ( b: . P(a,b)) | [split_int_domain_by_norm_lower] |
Thm* P:(     Prop), a: .
Thm* ( b:{a...}. ( c:{a..b }. P(a,c))  P(a,b))  ( b:{a...}. P(a,b)) | [int_seg_upper_ind] |
Thm* P:(     Prop).
Thm* ( a: , b:{...a}. P(a,b))
Thm* 
Thm* ( a: . ( b:{...a}. P(a,b))  ( b:{a...}. P(a,b)))  ( a,b: . P(a,b)) | [all_int_pairs_via_all_splits] |
Thm* P:(     Prop), a: .
Thm* ( b:{...a}. P(a,b))
Thm* 
Thm* (( b:{...a}. P(a,b))  ( b:{a...}. P(a,b)))  ( b: . P(a,b)) | [split_int_domain] |
Thm* f:(A A A), u,v:A. is_ident(A; f; u)  is_ident(A; f; v)  u = v | [binary_ident_unique] |