coe one

Stream: new members

[Maxime Darrin]

HI,
I want to apply nat.mul_one to an hypothesis involving pnats using rw, how can I somehow cast a pnat into a nat

import data.pnat.basic

theorem USAJMO_Problems_Problem_1 :
  forall f: pnat -> pnat,
  (forall (a b: pnat), f(a*a + b*b) = f(a)* f(b) /\ f(a*a) = f(a)*f(a))
  -> forall n, f n = 1 :=
  begin
  intro f,
  intro ab,

  have f1 : f(1) = 1,
  have f2 : f (1*1) = (f 1)*(f 1),
  exact and.elim_right (ab 1 1),
  rw nat.mul_one at f2,

[Eric Rodriguez]

you can just use the more general mul_one, which works for all groups

[Eric Rodriguez]

(weaker, even!)

[Maxime Darrin]

Oh thx !