proposition: Lemma Qplus_is_assoc : associative Qplus_is_bin_fun.
proof: Proof. Proof Qplus_assoc. Lemma Qplus_is_commut1 : commutes Qplus_is_bin_fun. Proof Qplus_comm. Lemma Qopp_wd : fun_wd (S1:=Q_as_CSetoid) (S2:=Q_as_CSetoid) Qopp. Proof. repeat intro. apply Qopp_comp; trivial. Qed.
imports: CoRN.model.structures.Qsec CoRN.algebra.CSetoidFun