proposition: Lemma a2x : forall (a : M) (x : nat), power (o' a a) x = power a (x + x).
proof: Proof. simple induction x; simpl in |- *. auto with arith. intros; simpl in |- *. rewrite <- plus_n_Sm. simpl in |- *. rewrite o'_assoc; elim H; auto with arith. Qed.
imports: Arith Constants