`{Funext} {R : Ring} (I J : Ideal R) : Coprime I J <~> hexists (fun '(((i ; p) , (j ; q)) : sig I * sig J) => i + j = ring_one). Proof. simpl. srapply equiv_iff_hprop. - intros c. pose (snd (c ring_one) tt) as d; clearbody d; clear c. strip_truncations. apply tr. induction d. + destruct x. * exists ((g ; s), (ring_zero; ideal_in_zero _)). apply rng_plus_zero_r. * exists ((ring_zero; ideal_in_zero _), (g ; s)). apply rng_plus_zero_l. + exists ((ring_zero; ideal_in_zero _), (ring_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 isleftideal. + apply sgt_in. right. by apply isleftideal. Defined.
Require Import Basics Types. Require Import Spaces.Finite.Fin. Require Import Classes.interfaces.canonical_names. Require Import Algebra.Rings.Ring. Require Import Algebra.Groups.Subgroup. Require Import Algebra.AbGroups. Require Import WildCat.Core. Module Import Notation.