(n : nat) : binary (Double1 n) = double1 (binary n). Proof. induction n. - reflexivity. - change (binary (Double1 n.+1)) with (Succ (Succ (binary (Double n).+1))). rewrite IHn. reflexivity. Qed.
Require Import Require Import Require Import