proposition: Lemma pow1 : forall n:nat, 1 ^ n = 1.
proof: Proof. intro; induction n as [| n Hrecn]. - reflexivity. - simpl; rewrite Hrecn; rewrite Rmult_1_r; reflexivity. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac