"takes longer"

NNG4/Game/Levels/Multiplication/L07mul_add.lean

Lines 49 to 56 in 18e0aec

    
           induction c with d hd 
        
           rw [add_zero, mul_zero, add_zero] 
        
           rfl 
        
           rw [add_succ, mul_succ, hd, mul_succ, add_assoc] 
        
           rfl 
        
           ``` 
        
           Inducting on `a` or `b` also works, but takes longer.

induction b with b hb
rw [zero_add, mul_zero, zero_add]
rfl
rw [succ_add, mul_succ, mul_succ, add_right_comm, hb]
rfl

Doesn't seem to take longer.

changed to "might take longer".

I think in a historic version not all of the reversed statements (zero_add, etc.) or add_right_comm might have not been available. The pedagogical thought here was that one should always start induction on the last variable because + is defined inductively on the second variable.

	induction c with d hd
	rw [add_zero, mul_zero, add_zero]
	rfl
	rw [add_succ, mul_succ, hd, mul_succ, add_assoc]
	rfl
	```

	Inducting on `a` or `b` also works, but takes longer.