proposition: Lemma distr_right_inst a b (mult : Z -> Z -> Z) : (forall x y z, mult (x + y) z =? mult x z + mult y z) -> (mult (3 + a) b =? mult 3 b + mult a b).
proof: Proof. intro H. verit H. Qed.
imports: SMTCoq.SMTCoq Bool ZArith