proposition: Lemma Tactic_lemmaF : forall (x y:F) (e:xexprF F val unop binop pfun x) (f:xexprF F val unop binop pfun y), expr_is_zero (NormF (xforgetF _ _ _ _ _ _ (xexprF_minus _ _ _ _ _ _ _ e f))) = true -> x[=]y.
proof: Proof. intros. apply cg_inv_unique_2. apply Tactic_lemma_zero_F with (xexprF_minus _ _ _ _ _ _ _ e f). assumption. Qed.
imports: CoRN.algebra.CFields CoRN.tactics.AlgReflection