proposition: Lemma mult_resp_Npos : bin_op_pres_pred _ NposP mult_as_bin_fun.
proof: Proof. intros x y H H0. unfold mult_as_bin_fun, NposP in |- *. apply mult_resp_Npos0; auto. Qed.
imports: CoRN.model.setoids.Nsetoid CoRN.model.structures.Npossec CoRN.algebra.CSetoidFun Coq(Lia)