proposition: Lemma copy_n_unit : forall j n, is_unit j = true -> eval (unit j) == @copy _ (Bin.value (e_bin i)) n (eval (unit j)).
proof: Proof. intros; induction n using Prect. rewrite copy_xH. reflexivity. rewrite copy_Psucc. rewrite <- IHn. apply is_unit_sum_Unit in H. rewrite law_neutral_left. reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)