proposition: Lemma is_eq_spec_pos : forall n m, if n ?= m then n = m else m <> n.
proof: Proof. intros n m; CaseEq (n ?= m);intro H. rewrite (is_eq_eq _ _ H);trivial. intro H1;rewrite H1 in H;rewrite is_eq_refl in H;discriminate H. Qed.
imports: ZArith Lia