proposition: Lemma get_signZ_th : sign_theory Z.opp Zeq_bool get_signZ.
proof: Proof. constructor. intros c;destruct c;intros ? H;try discriminate. injection H as [= <-]. simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom