proposition: Lemma binary_power_mult_equation (acc x:A)(n:nat) : binary_power_mult acc x n = match n with 0%nat => acc | _ => if Nat.Even_Odd_dec n then binary_power_mult acc (dot x x) (Nat.div2 n) else binary_power_mult (dot acc x) (dot x x) (Nat.div2 n) end.
proof: Proof. unfold binary_power_mult at 1. on_call binary_power_mult_func ltac:(fun c => unfold_sub @binary_power_mult_func c; fold binary_power_mult_func). cbn. destruct n; reflexivity. Qed.
imports: ZArith Arith Mat Program