Demo entry 6658401

KevinsMaths

   

Submitted by anonymous on Nov 07, 2017 at 00:28
Language: Lean. Code size: 314 Bytes.

theorem left_distrib (a b c : xnat) : (a + b) * c = a * c + b * c :=
begin
induction c with n Hn,
  unfold mul,
  refl,
rw [add_one_eq_succ,right_distrib,Hn,right_distrib,right_distrib],
rw [one,mul_one,mul_one,mul_one],
rw [add_assoc,add_assoc (b*n),add_comm (b*n),add_assoc,add_assoc,add_assoc],
end

This snippet took 0.00 seconds to highlight.

Back to the Entry List or Home.

Delete this entry (admin only).