proposition: Lemma ab_biprod_decompose {B A : AbGroup} (a : A) (b : B) : (a, b) = ((a, group_unit) : ab_biprod A B) + (group_unit, b).
proof: Proof. apply path_prod; cbn. - exact (right_identity _)^. - exact (left_identity _)^. Defined.
imports: Basics Types Truncations.Core WildCat HSet AbelianGroup Modalities.ReflectiveSubuniverse