proposition: Lemma power2_plus : forall x y : nat, power2 (x + y) = power2 x * power2 y.
proof: Proof. simple induction x. intros. simpl in |- *. elim plus_n_O; auto with arith. intros. simpl in |- *. rewrite H. rewrite mult_plus_distr_r. trivial with arith. Qed.
imports: Plus Mult Minus Lt Le Gt