(m : binnat) : toR (Succ m) = (toR m)+1. Proof. induction m. - change (2 * 0 + 1 = 0 + 1). rewrite mult_comm. rewrite mult_0_l. done. - change (2 * (toR m) + 2 = 2 * (toR m) + 1 + 1). apply plus_assoc. - induction m as [|m _|m _]. + change (2 * (2 * 0 + 1) + 1 = 2 * 0 + 2 + 1). rewrite plus_mult_distr_l. rewrite (@mult_1_r _ Aplus Amult Azero Aone H _). rewrite mult_0_r, mult_0_r. reflexivity. + change (2 * (2 * (toR m) + 2) + 1 = 2 * (2 * (toR m) + 1 ) + 2 + 1). apply (ap (fun z => z + 1)). assert (L : 2 * toR m + 2 = 2 * toR m + 1 + 1) by by rewrite plus_assoc. rewrite L; clear L. rewrite plus_mult_distr_l. rewrite mult_1_r. reflexivity. + simpl in IHm. change ((2 * (toR (double1 (Succ m))) + 1 = 2 * (toR (double2 m)) + 2 + 1)). rewrite IHm; clear IHm. rewrite plus_mult_distr_l. rewrite mult_1_r. reflexivity. Qed.
Require Import Require Import Require Import