:: Pascal's Triangle and {L}ucas's Theorem
:: by Rafa{\l} Ziobro
::
:: Received December 24, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

:: NAT_D

theorem ND1: :: NEWTON07:1

for k, n being non zero Nat st k mod n = 0 holds
(k - 1) mod n = n - 1

proof end;

theorem ND2: :: NEWTON07:2

for k being Nat
for n being non zero Nat st (k + 1) mod n = 0 holds
(k + 1) div n = (k div n) + 1

proof end;

registration

let a be non zero Nat;

reduce (a - 1) mod a to a - 1;

reducibility
(a - 1) mod a = a - 1

proof end;

end;

theorem ND3: :: NEWTON07:3

for n, k being non zero Nat st n mod k > 0 holds
(n - 1) mod k = (n mod k) - 1

proof end;

theorem ND4: :: NEWTON07:4

for n, k being non zero Nat st n mod k > 0 holds
n div k = (n - 1) div k

proof end;

:: Factorial

registration

let a be trivial Nat;

cluster a ! -> trivial non zero ;

coherence
( a ! is trivial & not a ! is zero )

proof end;

end;

registration

reduce 1 ! to 1;

reducibility
1 ! = 1 by NEWTON:13;

reduce 2 ! to 2;

reducibility
2 ! = 2 by NEWTON:14;
let a, b be Nat;

cluster ((a + b) !) mod b -> zero ;

coherence
((a + b) !) mod b is zero

proof end;

end;

theorem MDF: :: NEWTON07:5

for n, k being Nat holds n ! divides (n + k) !

proof end;

theorem MDF1: :: NEWTON07:6

for n, k being Nat holds (min (n,k)) ! divides n !

proof end;

registration

let n be Nat;

reduce n choose 1 to n;

reducibility
n choose 1 = n

proof end;

let k be Nat;

cluster ((n + k) !) / (n !) -> natural ;

coherence
((n + k) !) / (n !) is natural

proof end;

cluster ((n + k) !) / ((n !) * (k !)) -> natural ;

coherence
((n + k) !) / ((n !) * (k !)) is natural

proof end;

cluster (n !) / ((min (n,k)) !) -> natural ;

coherence
(n !) / ((min (n,k)) !) is natural

proof end;

cluster ((n + k) !) / (((min (n,k)) !) |^ 2) -> natural ;

coherence
((n + k) !) / (((min (n,k)) !) |^ 2) is natural

proof end;

end;

theorem FPD: :: NEWTON07:7

for n, k being Nat holds (n !) |^ k divides (n * k) !

proof end;

theorem :: NEWTON07:8

for n, k being Nat st k >= 2 * n holds
2 |^ n divides k !

proof end;

:: n choose k

registration

let n be non zero Nat;

reduce 0 choose n to 0 ;

reducibility
0 choose n = 0 by NEWTON:def 3;
let m be Nat;

cluster (m mod n) choose n -> zero ;

coherence
(m mod n) choose n is zero

proof end;

end;

theorem N20: :: NEWTON07:9

for k, n being Nat holds (k + n) choose n = (k + n) choose k

proof end;

theorem NP0: :: NEWTON07:10

for n being odd Nat holds n choose ((n + 1) / 2) = n choose ((n - 1) / 2)

proof end;

theorem NP1: :: NEWTON07:11

for n being Nat holds (2 * (n + 1)) choose (n + 1) = 2 * (((2 * n) + 1) choose n)

proof end;

theorem NP2: :: NEWTON07:12

for n being Nat holds ((n + 1) choose 2) - (n choose 2) = n

proof end;

registration

let n be Nat;

reduce (n + 1) choose 0 to 1;

reducibility
(n + 1) choose 0 = 1 by NEWTON:19;

reduce ((n + 1) choose 2) - (n choose 2) to n;

reducibility
((n + 1) choose 2) - (n choose 2) = n by NP2;

cluster (2 * (n + 1)) choose (n + 1) -> even ;

coherence
(2 * (n + 1)) choose (n + 1) is even

proof end;

end;

theorem NPP: :: NEWTON07:13

for n being Nat
for m being non zero Nat holds (n mod m) choose (m - 1) < 2

proof end;

registration

let m, n be Nat;

cluster (n mod (m + 1)) choose m -> trivial ;

coherence
(n mod (m + 1)) choose m is trivial

proof end;

end;

theorem NPR: :: NEWTON07:14

for n being Nat
for m being non zero Nat holds
( (n mod m) choose (m - 1) = 1 iff n mod m = m - 1 )

proof end;

theorem :: NEWTON07:15

for p being odd Prime holds p divides (p + 1) choose ((p + 1) / 2)

proof end;

theorem :: NEWTON07:16

for p being odd Prime
for k being non zero Nat st k + 1 < p holds
p divides (p + 1) choose (k + 1)

proof end;

theorem PCK: :: NEWTON07:17

for p being Prime
for k being non zero Nat st k <> p holds
(p choose k) mod p = 0

proof end;

theorem :: NEWTON07:18

for p being Prime
for k being non zero Nat st not p divides k holds
(p choose (k mod p)) mod p = 0

proof end;

LmPCZ: for p being odd Prime
for n being Nat st (2 * n) + 1 < p holds
( ((p - 1) choose (2 * n)) mod p = 1 & ((p - 1) choose ((2 * n) + 1)) mod p = p - 1 )

proof end;

theorem PCZ: :: NEWTON07:19

for p being Prime
for n being odd Nat st n < p holds
( ((p - 1) choose n) mod p = p - 1 & ((p - 1) choose (n - 1)) mod p = 1 )

proof end;

theorem :: NEWTON07:20

for p being Prime
for n being even Nat st n < p holds
((p - 1) choose n) mod p = 1

proof end;

theorem PC0: :: NEWTON07:21

for p being Prime
for n being Nat
for k being non zero Nat st n + k < p holds
((p + n) choose (k + n)) mod p = 0

proof end;

theorem :: NEWTON07:22

for p being Prime
for n being Nat st n + 2 < p holds
((p + 1) choose (n + 2)) mod p = 0

proof end;

theorem :: NEWTON07:23

for p being Prime
for n being Nat st n < p holds
((p + n) choose n) mod p = 1

proof end;

theorem PCM: :: NEWTON07:24

for p being Prime
for n, k being Nat st k <= n & n < p holds
((p + n) choose k) mod p = (n choose k) mod p

proof end;

theorem PCN: :: NEWTON07:25

for p being Prime
for n being non zero Nat st n < p holds
((2 * p) choose n) mod p = 0

proof end;

theorem :: NEWTON07:26

for p being Prime
for k, n being Nat st k < n & n <= p holds
((p + n) choose k) mod p = (n choose k) mod p

proof end;

theorem :: NEWTON07:27

for p being Prime
for n being Nat st not p divides n holds
(p choose n) mod p = 0

proof end;

theorem ILO: :: NEWTON07:28

for a, b being non zero Nat holds ((a * b) choose 1) mod b = 0

proof end;

theorem :: NEWTON07:29

for a, b being Nat holds (((a * b) + 1) choose 1) mod b = 1 mod b

proof end;

theorem CPP: :: NEWTON07:30

for a, b, c being Nat holds ((a + 1) choose (b + 1)) mod c = (((a choose b) mod c) + ((a choose (b + 1)) mod c)) mod c

proof end;

theorem CPK: :: NEWTON07:31

for p being Prime
for n, k being Nat st k <> p holds
(((n mod p) + 1) choose k) mod p = (((n + 1) mod p) choose k) mod p

proof end;

:: recurrence of PT mod p
:: Anton's lemma

theorem AL: :: NEWTON07:32

for p being Prime
for n, k being Nat holds (n choose k) mod p = (((n mod p) choose (k mod p)) * ((n div p) choose (k div p))) mod p

proof end;

theorem :: NEWTON07:33

for p being Prime
for n being Nat holds (n choose p) mod p = (n div p) mod p

proof end;

theorem :: NEWTON07:34

for p being Prime
for n being Nat holds ((p + n) choose p) mod p = ((n div p) + 1) mod p

proof end;

theorem :: NEWTON07:35

for p being Prime
for n being Nat holds ((p * n) choose p) mod p = n mod p

proof end;

:: the way below is obviously ineffective for proving AL, remove if you wish

theorem MOC: :: NEWTON07:36

for p being Prime
for n, k being Nat st k < p holds
(n choose k) mod p = ((n mod p) choose k) mod p

proof end;

theorem NPK: :: NEWTON07:37

for n, k being Nat
for p being Prime st k < p holds
(((n * p) + k) choose k) mod p = 1

proof end;

theorem KPN: :: NEWTON07:38

for n, k being Nat
for p being Prime st k < p holds
(((n * p) + k) choose (n * p)) mod p = 1

proof end;

theorem :: NEWTON07:39

for p being Prime holds ((2 * p) choose p) mod p = 2 mod p

proof end;

theorem :: NEWTON07:40

for p being Prime
for n being Nat holds (n choose (p - 1)) mod p = ((n mod p) choose (p - 1)) mod p

proof end;

theorem IPN: :: NEWTON07:41

for k being non zero Nat
for i being Nat
for p being Prime holds (((i * p) + (p -' k)) choose (p -' k)) mod p = 1

proof end;

theorem KPW: :: NEWTON07:42

for p being Prime
for n, k being Nat st k < p holds
(((n * p) + k) choose p) mod p = ((n * p) choose p) mod p

proof end;

theorem :: NEWTON07:43

for p being Prime
for n, k being Nat holds (((n + k) * p) choose p) mod p = (n + k) mod p

proof end;

theorem :: NEWTON07:44

for p being Prime
for k, n being Nat
for m being non zero Nat st k + m < p holds
(((n * p) + k) choose (m + k)) mod p = 0

proof end;

theorem PAS: :: NEWTON07:45

for n being Nat holds Parity ((n + 1) !) = (Parity (n + 1)) * (Parity (n !))

proof end;

theorem :: NEWTON07:46

for n being even Nat holds Parity (n !) = Parity ((n + 1) !)

proof end;

theorem :: NEWTON07:47

for n being Nat holds Parity ((n + 2) !) = (2 * (Parity (Triangle (n + 1)))) * (Parity (n !))

proof end;

:: Pascal's Triangle step by step:

registration

let f be 1 -element FinSequence;

reduce <*(f . 1)*> to f;

reducibility
<*(f . 1)*> = f

proof end;

end;

registration

let f be 2 -element FinSequence;

reduce <*(f . 1),(f . 2)*> to f;

reducibility
<*(f . 1),(f . 2)*> = f

proof end;

end;

registration

let f be 3 -element FinSequence;

reduce <*(f . 1),(f . 2),(f . 3)*> to f;

reducibility
<*(f . 1),(f . 2),(f . 3)*> = f

proof end;

end;

registration

let f be 4 -element FinSequence;

reduce <*(f . 1),(f . 2),(f . 3),(f . 4)*> to f;

reducibility
<*(f . 1),(f . 2),(f . 3),(f . 4)*> = f

proof end;

end;

registration

let f be 5 -element FinSequence;

reduce <*(f . 1),(f . 2),(f . 3),(f . 4),(f . 5)*> to f;

reducibility
<*(f . 1),(f . 2),(f . 3),(f . 4),(f . 5)*> = f

proof end;

end;

registration

let f be 6 -element FinSequence;

reduce <*(f . 1),(f . 2),(f . 3),(f . 4),(f . 5),(f . 6)*> to f;

reducibility
<*(f . 1),(f . 2),(f . 3),(f . 4),(f . 5),(f . 6)*> = f

proof end;

end;

registration

let f be 7 -element FinSequence;

reduce <*(f . 1),(f . 2),(f . 3),(f . 4),(f . 5),(f . 6),(f . 7)*> to f;

reducibility
<*(f . 1),(f . 2),(f . 3),(f . 4),(f . 5),(f . 6),(f . 7)*> = f

proof end;

end;

registration

let f be 8 -element FinSequence;

reduce <*(f . 1),(f . 2),(f . 3),(f . 4),(f . 5),(f . 6),(f . 7),(f . 8)*> to f;

reducibility
<*(f . 1),(f . 2),(f . 3),(f . 4),(f . 5),(f . 6),(f . 7),(f . 8)*> = f

proof end;

end;

registration

let n be Nat;

reduce <*0*> . n to 0 ;

reducibility
<*0*> . n = 0

proof end;

end;

registration

let a1, a2, a3, a4, a5 be Complex;

cluster <*a1,a2,a3,a4,a5*> -> complex-valued ;

coherence
<*a1,a2,a3,a4,a5*> is complex-valued

proof end;

let a6 be Complex;

cluster <*a1,a2,a3,a4,a5,a6*> -> complex-valued ;

coherence
<*a1,a2,a3,a4,a5,a6*> is complex-valued

proof end;

let a7 be Complex;

cluster <*a1,a2,a3,a4,a5,a6,a7*> -> complex-valued ;

coherence
<*a1,a2,a3,a4,a5,a6,a7*> is complex-valued

proof end;

let a8 be Complex;

cluster <*a1,a2,a3,a4,a5,a6,a7,a8*> -> complex-valued ;

coherence
<*a1,a2,a3,a4,a5,a6,a7,a8*> is complex-valued

proof end;

end;

:: FINSEQ_1:65

theorem FINSEQ165: :: NEWTON07:48

for n being non zero Nat
for f, g being FinSequence holds (f ^ g) . ((len f) + n) = g . n

proof end;

theorem CF: :: NEWTON07:49

for n being non zero Nat
for c being Complex
for f being FinSequence holds (<*c*> ^ f) . (n + 1) = f . n

proof end;

theorem FINSEQ1D7: :: NEWTON07:50

for f being FinSequence
for n being Nat holds (f ^ <*0*>) . n = f . n

proof end;

theorem PT: :: NEWTON07:51

for n being Nat holds Newton_Coeff (n + 1) = (<*0*> ^ (Newton_Coeff n)) + ((Newton_Coeff n) ^ <*0*>)

proof end;

theorem FINSEQ940A: :: NEWTON07:52

for a1, a2, b1, b2 being Complex
for n being Nat
for f, g being b₅ -element complex-valued FinSequence holds (f ^ <*a1,a2*>) + (g ^ <*b1,b2*>) = (f + g) ^ <*(a1 + b1),(a2 + b2)*>

proof end;

theorem FINSEQ940B: :: NEWTON07:53

for a1, a2, a3, b1, b2, b3 being Complex
for n being Nat
for f, g being b₇ -element complex-valued FinSequence holds (f ^ <*a1,a2,a3*>) + (g ^ <*b1,b2,b3*>) = (f + g) ^ <*(a1 + b1),(a2 + b2),(a3 + b3)*>

proof end;

theorem A5B5: :: NEWTON07:54

for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being Complex holds <*a1,a2,a3,a4,a5*> + <*b1,b2,b3,b4,b5*> = <*(a1 + b1),(a2 + b2),(a3 + b3),(a4 + b4),(a5 + b5)*>

proof end;

theorem A6B6: :: NEWTON07:55

for a1, a2, a3, a4, a5, a6, b1, b2, b3, b4, b5, b6 being Complex holds <*a1,a2,a3,a4,a5,a6*> + <*b1,b2,b3,b4,b5,b6*> = <*(a1 + b1),(a2 + b2),(a3 + b3),(a4 + b4),(a5 + b5),(a6 + b6)*>

proof end;

theorem A7B7: :: NEWTON07:56

for a1, a2, a3, a4, a5, a6, a7, b1, b2, b3, b4, b5, b6, b7 being Complex holds <*a1,a2,a3,a4,a5,a6,a7*> + <*b1,b2,b3,b4,b5,b6,b7*> = <*(a1 + b1),(a2 + b2),(a3 + b3),(a4 + b4),(a5 + b5),(a6 + b6),(a7 + b7)*>

proof end;

theorem A8B8: :: NEWTON07:57

for a1, a2, a3, a4, a5, a6, a7, a8, b1, b2, b3, b4, b5, b6, b7, b8 being Complex holds <*a1,a2,a3,a4,a5,a6,a7,a8*> + <*b1,b2,b3,b4,b5,b6,b7,b8*> = <*(a1 + b1),(a2 + b2),(a3 + b3),(a4 + b4),(a5 + b5),(a6 + b6),(a7 + b7),(a8 + b8)*>

proof end;

theorem NC0: :: NEWTON07:58

Newton_Coeff 0 = <*1*>

proof end;

theorem :: NEWTON07:59

Newton_Coeff 1 = <*1,1*>

proof end;

theorem :: NEWTON07:60

Newton_Coeff 2 = <*1,2,1*>

proof end;

theorem NC3: :: NEWTON07:61

Newton_Coeff 3 = <*1,3,3,1*>

proof end;

theorem NC4: :: NEWTON07:62

Newton_Coeff 4 = <*1,4,6,4,1*>

proof end;

theorem NC5: :: NEWTON07:63

Newton_Coeff 5 = <*1,5,10,10,5,1*>

proof end;

theorem NC6: :: NEWTON07:64

Newton_Coeff 6 = <*1,6,15,20,15,6,1*>

proof end;

theorem NC7: :: NEWTON07:65

Newton_Coeff 7 = <*1,7,21,35,35,21,7,1*>

proof end;

theorem :: NEWTON07:66

Newton_Coeff 8 = <*1,8,28,56,70,56,28,8,1*>

proof end;

:: The Little Hockey Stick and Puck Theorem

theorem :: NEWTON07:67

for n being Nat holds ((n choose 0) + ((n + 2) choose 1)) + ((n + 4) choose 2) = ((n + 5) choose 2) - ((n + 5) choose 0)

proof end;

:: The Big Hockey Stick and Puck Theorem

theorem :: NEWTON07:68

for n being Nat holds (((n choose 0) + ((n + 2) choose 1)) + ((n + 4) choose 2)) + ((n + 6) choose 3) = ((n + 7) choose 3) - ((n + 6) choose 1)

proof end;

theorem LmN: :: NEWTON07:69

for n, k being Nat st k in Seg (n + 1) holds
ex l, m being Nat st
( l = k - 1 & m = n - l )

proof end;

theorem :: NEWTON07:70

for a, b being Complex
for n, k being Nat st k in Seg (n + 1) holds
ex c being object ex l, m being Nat st
( m = k - 1 & l = n - m & c = (a |^ l) * (b |^ m) )

proof end;

:: Pascal's Triangle: https://oeis.org/A007318
:: Harmonic Triangle, https://www.deltami.edu.pl/media/articles/2020/02/delta-2020-02-trojkat-harmoniczny-blizniak-trojkata-pascala.pdf

definition

let n be non zero Nat;

func RHartr n -> FinSequence equals :: NEWTON07:def 1
n (#) (Newton_Coeff (n - 1));

coherence
n (#) (Newton_Coeff (n - 1)) is FinSequence ;

end;

:: deftheorem defines RHartr NEWTON07:def 1 :
for n being non zero Nat holds RHartr n = n (#) (Newton_Coeff (n - 1));

registration

let n be non zero Nat;

cluster RHartr n -> n -element ;

coherence
RHartr n is n -element ;

cluster RHartr n -> NAT -valued ;

coherence
RHartr n is NAT -valued ;

end;

theorem HAR: :: NEWTON07:71

for n, k being non zero Nat holds (RHartr n) . k = n * ((n - 1) choose (k - 1))

proof end;

theorem :: NEWTON07:72

RHartr 1 = <*1*> by NC0;

theorem RH2: :: NEWTON07:73

RHartr 2 = <*2,2*>

proof end;

theorem RH3: :: NEWTON07:74

RHartr 3 = <*3,6,3*>

proof end;

theorem RH4: :: NEWTON07:75

RHartr 4 = <*4,12,12,4*>

proof end;

theorem RH5: :: NEWTON07:76

RHartr 5 = <*5,20,30,20,5*>

proof end;

theorem RH6: :: NEWTON07:77

RHartr 6 = <*6,30,60,60,30,6*>

proof end;

theorem RH7: :: NEWTON07:78

RHartr 7 = <*7,42,105,140,105,42,7*>

proof end;

theorem RH8: :: NEWTON07:79

RHartr 8 = <*8,56,168,280,280,168,56,8*>

proof end;

definition

let n be non zero Nat;

:: :Def3:

func Hartr n -> FinSequence equals :: NEWTON07:def 2
(RHartr n) " ;

coherence
(RHartr n) " is FinSequence ;

end;

:: deftheorem defines Hartr NEWTON07:def 2 :
for n being non zero Nat holds Hartr n = (RHartr n) " ;

registration

let n be non zero Nat;

cluster Hartr n -> n -element ;

coherence
Hartr n is n -element ;

cluster Hartr n -> REAL -valued ;

coherence
Hartr n is REAL -valued ;

end;

theorem :: NEWTON07:80

for n, k being non zero Nat holds (Hartr n) . k = 1 / (n * ((n - 1) choose (k - 1)))

proof end;

theorem :: NEWTON07:81

for n being non zero Nat holds Sum (RHartr n) = n * (2 |^ (n - 1))

proof end;

theorem :: NEWTON07:82

Hartr 1 = <*1*>

proof end;

theorem :: NEWTON07:83

Hartr 2 = <*(1 / 2),(1 / 2)*>

proof end;

theorem :: NEWTON07:84

Hartr 3 = <*(1 / 3),(1 / 6),(1 / 3)*>

proof end;

theorem :: NEWTON07:85

Hartr 4 = <*(1 / 4),(1 / 12),(1 / 12),(1 / 4)*>

proof end;

theorem :: NEWTON07:86

Hartr 5 = <*(1 / 5),(1 / 20),(1 / 30),(1 / 20),(1 / 5)*>

proof end;

theorem :: NEWTON07:87

Hartr 6 = <*(1 / 6),(1 / 30),(1 / 60),(1 / 60),(1 / 30),(1 / 6)*>

proof end;

theorem :: NEWTON07:88

Hartr 7 = <*(1 / 7),(1 / 42),(1 / 105),(1 / 140),(1 / 105),(1 / 42),(1 / 7)*>

proof end;

theorem :: NEWTON07:89

Hartr 8 = <*(1 / 8),(1 / 56),(1 / 168),(1 / 280),(1 / 280),(1 / 168),(1 / 56),(1 / 8)*>

proof end;

:: https://mathworld.wolfram.com/RascalTriangle.html

definition

let n be natural Number ;

func Rascal n -> FinSequence means :Def1: :: NEWTON07:def 3
( dom it = Seg (n + 1) & ( for i being Nat st i in dom it holds
it . i = ((i - 1) * ((n + 1) - i)) + 1 ) );

existence
ex b₁ being FinSequence st
( dom b₁ = Seg (n + 1) & ( for i being Nat st i in dom b₁ holds
b₁ . i = ((i - 1) * ((n + 1) - i)) + 1 ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence st dom b₁ = Seg (n + 1) & ( for i being Nat st i in dom b₁ holds
b₁ . i = ((i - 1) * ((n + 1) - i)) + 1 ) & dom b₂ = Seg (n + 1) & ( for i being Nat st i in dom b₂ holds
b₂ . i = ((i - 1) * ((n + 1) - i)) + 1 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Rascal NEWTON07:def 3 :
for n being natural Number
for b₂ being FinSequence holds
( b₂ = Rascal n iff ( dom b₂ = Seg (n + 1) & ( for i being Nat st i in dom b₂ holds
b₂ . i = ((i - 1) * ((n + 1) - i)) + 1 ) ) );

registration

let n be Nat;

cluster Rascal n -> n + 1 -element ;

coherence
Rascal n is n + 1 -element

proof end;

end;

theorem :: NEWTON07:90

Rascal 0 = <*1*>

proof end;

theorem :: NEWTON07:91

Rascal 1 = <*1,1*>

proof end;

theorem :: NEWTON07:92

Rascal 2 = <*1,2,1*>

proof end;

theorem :: NEWTON07:93

Rascal 3 = <*1,3,3,1*>

proof end;

theorem :: NEWTON07:94

Rascal 4 = <*1,4,5,4,1*>

proof end;

theorem :: NEWTON07:95

Rascal 5 = <*1,5,7,7,5,1*>

proof end;

theorem :: NEWTON07:96

Rascal 6 = <*1,6,9,10,9,6,1*>

proof end;

theorem R7: :: NEWTON07:97

Rascal 7 = <*1,7,11,13,13,11,7,1*>

proof end;

theorem :: NEWTON07:98

(Rascal 7) . 4 = 13 by R7;

theorem :: NEWTON07:99

for n being Nat holds (Rascal n) . 1 = 1

proof end;

theorem :: NEWTON07:100

for n being non zero Nat holds (Rascal n) . 2 = n

proof end;

registration

let n, m be Nat;

cluster (Rascal n) . m -> natural ;

coherence
(Rascal n) . m is natural

proof end;

end;

:: https://www.artofmathematics.org/sites/default/files/rascalstackled.pdf

theorem :: NEWTON07:101

for k, n being Nat holds ((Rascal (k + n)) . (n + 1)) + ((Rascal ((k + n) + 2)) . (n + 2)) = (((Rascal ((k + n) + 1)) . (n + 1)) + ((Rascal ((k + n) + 1)) . (n + 2))) + 1

proof end;

theorem :: NEWTON07:102

for k, n being Nat holds ((Rascal (k + n)) . (n + 1)) * ((Rascal ((k + n) + 2)) . (n + 2)) = (((Rascal ((k + n) + 1)) . (n + 1)) * ((Rascal ((k + n) + 1)) . (n + 2))) + 1

proof end;