proposition: Lemma eq0_cnf : forall x, (0 < x -> False) /\ (0 < - x -> False) <-> x == 0.
proof: Proof. intros x; split ; intros H. + apply (SORle_antisymm sor). * now rewrite (Rle_ngt sor). * rewrite (Rle_ngt sor). rewrite (Rlt_lt_minus sor). setoid_replace (0 - x) with (-x) by ring. tauto. + split; intro H0. * rewrite (SORlt_le_neq sor) in H0. apply (proj2 H0). now rewrite H. * rewrite (SORlt_le_neq sor) in H0. apply (proj2 H0). rewrite H. ring. Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl