proposition: Lemma binary_power_mult_ok : forall n a x, binary_power_mult a x n = a * x ** n.
proof: Proof. intro n; pattern n;apply lt_wf_ind. clear n; intros n Hn; destruct n. - intros;simpl; monoid_simpl; trivial. - intros; rewrite binary_power_mult_equation. destruct (Nat.Even_Odd_dec (S n)). rewrite Hn, power_of_square; factorize. pattern (S n) at 3;replace (S n) with (Nat.div2 (S n) + Nat.div2 (S n))%nat;auto. generalize (Nat.Even_double _ e);simpl;auto. apply Nat.lt_div2;auto with arith. rewrite Hn. rewrite power_of_square ; factorize. pattern (S n) at 3;replace (S n) with (S (Nat.div2 (S n) + Nat.div2 (S n)))%nat; auto. rewrite <- dot_assoc; factorize;auto. generalize (Nat.Odd_double _ o);intro H;auto. apply Nat.lt_div2;auto with arith. Qed.
imports: ZArith Arith Mat Program