proposition: Lemma check_inconsistent_sound : forall (p : PolC) (op : Op1), check_inconsistent (p, op) = true -> forall env, ~ eval_op1 op (eval_pol env p).
proof: Proof. intros p op H1 env. unfold check_inconsistent in H1. destruct op; simpl ; destruct p ; simpl; try discriminate H1; try rewrite <- (morph0 (SORrm addon)); trivial. - now apply cneqb_sound. - apply (morph_eq (SORrm addon)) in H1. congruence. - apply cleb_sound in H1. now apply -> (Rle_ngt sor). - apply cltb_sound in H1. now apply -> (Rlt_nge sor). Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl