proposition: Lemma equiv_coprime_sum `{Funext} {R : CRing} (I J : Ideal R) : Coprime I J <~> hexists (fun '(((i ; p) , (j ; q)) : sig I * sig J) => i + j = cring_one).
proof: Proof. simpl. srapply equiv_iff_hprop. { intros c. pose (snd (c cring_one) tt) as d; clearbody d; clear c. strip_truncations. apply tr. induction d. - destruct x. + exists ((g ; s), (cring_zero; ideal_in_zero _)). apply rng_plus_zero_r. + exists ((cring_zero; ideal_in_zero _), (g ; s)). apply rng_plus_zero_l. - exists ((cring_zero; ideal_in_zero _), (cring_zero; ideal_in_zero _)). apply rng_plus_zero_l. - destruct IHd1 as [[[x xi] [y yj]] p]. destruct IHd2 as [[[w wi] [z zj]] q]. srefine (((_;_),(_;_));_). + exact (x - w). + by apply ideal_in_plus_negate. + exact (y - z). + by apply ideal_in_plus_negate. + cbn. refine (_ @ ap011 (fun x y => x - y) p q). rewrite <- 2 rng_plus_assoc. f_ap. rewrite negate_sg_op. rewrite rng_plus_comm. rewrite rng_plus_assoc. reflexivity. } intro x. strip_truncations. intros r. split;[intro; exact tt|]. intros _. destruct x as [[[x xi] [y yj]] p]. rewrite <- rng_mult_one_r. change (x + y = 1) in p. rewrite <- p. rewrite rng_dist_l. apply tr. rapply sgt_op'. - apply sgt_in. left. by apply isideal. - apply sgt_in. right. by apply isideal. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups