proposition: Lemma plus_resp_Npos : bin_op_pres_pred _ NposP plus_is_bin_fun.
proof: Proof. unfold bin_op_pres_pred in |- *. simpl in |- *. apply plus_resp_Npos0. Qed.
imports: CoRN.model.setoids.Nsetoid CoRN.model.structures.Npossec CoRN.algebra.CSetoidFun Coq(Lia)