proposition: Lemma ZSORaddon : SORaddon 0 1 Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool Z.leb (fun x => x) (fun x => x) (pow_N 1 Z.mul).
proof: Proof. constructor. - constructor ; intros ; try reflexivity. apply Zeq_bool_eq ; auto. - constructor. reflexivity. - intros x y. apply Zeq_bool_neq ; auto. - apply Zle_bool_imp_le. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing