coq - How to prove binary commutavity with a different definition of bin? -

// collacoq link: https://x80.org/collacoq/qezicaroni.coq  inductive bin : type := | 0 : bin | 1 : bin | zerop : bin -> bin | onep : bin -> bin.  inductive bin_carry : type := | zeroc : bin_carry | onec : bin_carry.  (*returns carry, new_state*) fixpoint incr' (x : bin) : bin_carry * bin :=   match x   | 0 => (zeroc, one)   | 1 => (onec, zero)   | zerop x =>     match incr' x     | (onec, x') => (zeroc, onep x')     | (zeroc, x') => (zeroc, zerop x')     end   | onep x =>     match incr' x     | (onec, x') => (onec, zerop x')     | (zeroc, x') => (zeroc, onep x')     end   end.   definition incr (x : bin): bin :=   match incr' x   | (zeroc,x) => x   | (onec,x) => onep x   end.  (*index_multiplier * result*) fixpoint bin_to_nat' (x : bin): nat * nat :=   match x   | 0 => (2,0)   | 1 => (2,1)   | zerop x =>     match bin_to_nat' x     | (multiplier,result) => (multiplier * 2,result)     end   | onep x =>     match bin_to_nat' x     | (multiplier,result) => (multiplier * 2,result + multiplier)     end   end.   definition bin_to_nat (x : bin): nat :=   match bin_to_nat' x   | (_,r) => r   end.  example bin_test1: bin_to_nat 0 = 0. proof. reflexivity. qed. example bin_test2: bin_to_nat (incr zero) = 1. proof. reflexivity. qed. example bin_test3: bin_to_nat (incr (incr zero)) = 2. proof. reflexivity. qed. example bin_test4: bin_to_nat (incr (incr (incr zero))) = 3. proof. reflexivity. qed. example bin_test5: bin_to_nat (incr (incr (incr (incr zero)))) = 4. proof. reflexivity. qed.  theorem binary_commute :   forall (x: bin),     bin_to_nat(incr x) = s (bin_to_nat x). proof. induction x.        - reflexivity.        - reflexivity.        - replace (zerop x) x.          + rewrite -> ihx. reflexivity.          + induction x.            * abort. 

i going through software foundations book , stumped on above. looked around on net , found the solution different kind of bin formulation, not think solution there applies here.

the trouble in third - bullet bin_to_nat (incr (zerop x)) = s (bin_to_nat (zerop x) not simplify , neither can rewritten directly. after learning replace thought might work, stuck trying prove zero = zerop zero.

i know problem states free change formulation of bin make proving commutativity easier, hunch not going far coq if stuck @ above definition. though unlike past few times, not think have tools past yet.

what missing here?

replace (zerop x) x. cannot succeed: such equation hold x need infinite term equal zerop (zerop (zerop (...))). may want prove first incr extensional semantically. i.e.

theorem incr_ext : forall (x y : bin),   bin_to_nat x = bin_to_nat y -> bin_to_nat (incr x) = bin_to_nat (incr y).