proposition: Lemma power_sym : forall (a : M) (n p : nat), o' (power a n) (power a p) = o' (power a p) (power a n).
proof: Proof. intros. rewrite <- power_plus. rewrite <- power_plus. rewrite plus_comm; auto with arith. Qed.
imports: Arith Constants