proposition: Lemma plus_is_fun : bin_fun_strext _ _ _ plus.
proof: Proof. intros x x' y y' H. elim (ap_cotransitive_unfolded _ _ _ H (plus x y')); intro H'. right; apply plus_lext with x. astepl (plus x y); astepr (plus x y'); auto. left; eauto. Qed.
imports: CoRN.algebra.CGroups