proposition: Lemma cneqb_sound : forall x y : C, x [~=] y = true -> [x] ~= [y].
proof: Proof. intros x y H1. apply (SORcneqb_morph addon). unfold cneqb, negb in H1. destruct (ceqb x y); now try discriminate. Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl