proposition: Lemma implb_ok : forall x, implb (bP x) (bQ x) = true <-> (P x -> Q x).
proof: Proof. intro x. unfold implb. case_eq (bP x). rewrite bP_ok, bQ_ok. tauto. rewrite (ko bP_ok). tauto. Qed.
imports: Coq(ZArith Lia) CoLoR(LogicUtil)