proposition: Lemma pow_exp : forall x y : R, forall e : nat, (x^e * y^e = (x*y)^e)%R.
proof: Proof. intros x y e. induction e. apply Rmult_1_l. repeat rewrite <- tech_pow_Rmult. rewrite <- IHe. ring. Qed.
imports: Flocq.Core.Defs Gappa_common