proposition: Lemma M2q : forall q : nat, gencode (Call_M (two_power q)).
proof: Proof. refine (let t := fun q : nat => gencode (Call_M (two_power q)) in (fix M2q (q : nat) : t q := match q as x return (t x) with | O => gencode_intro _ End _ | S p => match M2q p with | gencode_intro c s => gencode_intro _ (seq SQR c) _ end end)). constructor 1. unfold power in |- *; simpl in |- *. intros; rewrite (u_neutral_r M MO); auto with arith. constructor 1; auto with arith. intros; simpl in |- *. inversion_clear s. rewrite H. apply Config_inv; auto with arith. rewrite <- plus_n_O. apply a2x; auto with arith. Qed.
imports: Constants monoid spec machine Wf_compl Plus Mult Lt Mult_compl euclid two_power