proposition: Lemma fact_simpl : forall n:nat, fact (S n) = (S n * fact n)%nat.
proof: Proof. intro; reflexivity. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac