proposition: Lemma expr_is_zero_corr_F : forall e:expr, wfF F val unop binop pfun e -> expr_is_zero e = true -> II e [0].
proof: Proof. unfold wfF in |- *. intros e H. elim H. intro. elim e; simpl in |- *; try (intros; exfalso; inversion H0; fail). intros e0 H0 e1 H1. elim e0; simpl in |- *; try (intros; exfalso; inversion H2; fail). intro. elim z; simpl in |- *; try (intros; exfalso; inversion H2; fail); intros H2 H3. inversion H2. try (rewrite H4 in X; rewrite H6 in X0; rewrite H5 in H7). apply interpF_div with ([0]:F) y nzy; auto. algebra. apply (interpF_int F val unop binop pfun 0); algebra. Qed.
imports: CoRN.algebra.CFields CoRN.tactics.AlgReflection