proposition: Theorem firstNormalPosNormal : Fnormal firstNormalPos.
proof: Proof. repeat split; unfold firstNormalPos in |- *; simpl in |- *; auto with zarith. rewrite pGivesBound. rewrite Z.abs_eq; auto with zarith. unfold nNormMin in |- *; simpl in |- *. apply Zpower_nat_monotone_lt; auto with zarith. apply Zlt_le_weak;apply nNormPos. rewrite pGivesBound. replace precision with (pred precision + 1). rewrite Zpower_nat_is_exp; auto with zarith. rewrite Zpower_nat_1; auto with zarith. rewrite (fun x => Zmult_comm x radix); unfold nNormMin in |- *; lia. lia. Qed.
imports: Reals ZArith List PeanoNat Psatz