proposition: Lemma reduce_poly_of_formula_sound_alt : forall var fl fr, reduce (poly_add (poly_of_formula fl) (poly_of_formula fr)) = Cst false -> formula_eval var fl = formula_eval var fr.
proof: Proof. intros var fl fr Heq. repeat rewrite <- poly_of_formula_eval_compat. destruct (poly_of_formula_valid_compat fl) as [nl Hl]. destruct (poly_of_formula_valid_compat fr) as [nr Hr]. rewrite <- (reduce_eval_compat nl (poly_of_formula fl)); auto. rewrite <- (reduce_eval_compat nr (poly_of_formula fr)); auto. rewrite <- xorb_false_l; change false with (eval var (Cst false)). rewrite <- poly_add_compat, <- Heq. repeat rewrite poly_add_compat. rewrite (reduce_eval_compat nl); [|assumption]. rewrite (reduce_eval_compat (Pos.max nl nr)); [|apply poly_add_valid_compat; assumption]. rewrite (reduce_eval_compat nr); [|assumption]. rewrite poly_add_compat; ring. Qed.
imports: Bool DecidableClass Algebra Ring PArith Lia