proposition: Theorem strong_spec_red : forall x, [red x] = Qred [x].
proof: Proof. intros [ z | n d ]. unfold red. symmetry; apply Qred_identity; simpl; auto with zarith. unfold red; apply strong_spec_norm. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig