Require Import UniMath.PAdics.lemmas.
Require Import UniMath.Algebra.RigsAndRings.
Require Import UniMath.Algebra.Domains_and_Fields.

Local Open Scope ring_scope.

Section aint.

Variable A : aintdom.

Ltac permute := solve
  [
    repeat rewrite ringassoc2;
    match goal with
    | [ |- ?X = ?X ] ⇒ apply idpath
    | [ |- ?X × ?Y = ?X × ?Z ] ⇒ apply maponpaths; permute
    | [ |- ?Y × ?X = ?Z × ?X ] ⇒ apply ( maponpaths ( fun x ⇒ x × X ) ); permute
    | [ |- ?X × ?Y = ?Y × ?X ] ⇒ apply ringcomm2
    | [ |- ?X × ?Y = ?K ] ⇒ solve
             [
               repeat rewrite <- ringassoc2;
               match goal with
               | [ |- ?H = ?V × X ] ⇒ rewrite ( @ringcomm2 A V X );
                                     repeat rewrite ringassoc2;
                                     apply maponpaths;
                                     permute
               end
             | repeat rewrite ringassoc2;
               match goal with
               | [ |- ?H = ?Z × ?V ] ⇒ repeat rewrite <- ringassoc2;
                                       match goal with
                                       | [ |- ?W × Z = ?L ] ⇒ rewrite ( @ringcomm2 A W Z );
                                                              repeat rewrite ringassoc2;
                                                              apply maponpaths;
                                                              permute
                                       end
               end
             ]
    | [ |- ?X × ( ?Y × ?Z ) = ?K ] ⇒ rewrite ( @ringcomm2 A Y Z ); permute
    end
  | repeat rewrite <- ringassoc2;
    match goal with
    | [ |- ?X × ?Y = ?X × ?Z ] ⇒ apply maponpaths; permute
    | [ |- ?Y × ?X = ?Z × ?X ] ⇒ apply ( maponpaths ( fun x ⇒ x × X ) ); permute
    | [ |- ?X × ?Y = ?Y × ?X ] ⇒ apply ringcomm2
    end
  | apply idpath
  | idtac "The tactic permute does not apply to the current goal!"
  ].

Lemma azerorelcomp ( cd : A × aintdomazerosubmonoid A )
  ( ef : A × aintdomazerosubmonoid A )
  ( p : pr1 cd × pr1 ( pr2 ef ) =
        pr1 ef × pr1 ( pr2 cd ) )
  ( q : pr1 cd # 0 ) : pr1 ef # 0.
Proof.
  intros.
  change ( @op2 A ( pr1 cd ) ( pr1 ( pr2 ef ) ) =
           @op2 A ( pr1 ef ) ( pr1 ( pr2 cd ) ) ) in p.
  assert ( ( @op2 A ( pr1 cd ) ( pr1 ( pr2 ef ) ) ) # 0 ) as v.
  { apply A.
    assumption.
    apply ( pr2 ( pr2 ef ) ).
  }
  rewrite p in v.
  apply ( pr1 ( timesazero v ) ).
Defined.

Lemma azerolmultcomp { a b c : A } ( p : a # 0 ) ( q : b # c ) : a × b # a × c.
Proof.
  intros.
  apply aminuszeroa.
  rewrite <- ringminusdistr.
  apply ( pr2 A ).
  - assumption.
  - apply aaminuszero.
    assumption.
Defined.

Lemma azerormultcomp { a b c : A } ( p : a # 0 ) ( q : b # c ) : b × a # c × a.
Proof.
  intros.
  rewrite ( @ringcomm2 A b ).
  rewrite ( @ringcomm2 A c ).
  apply ( azerolmultcomp p q ).
Defined.

Definition afldfracapartrelpre : hrel ( A × aintdomazerosubmonoid A ) :=
  fun ab cd ⇒ ( pr1 ab × pr1 ( pr2 cd ) ) # ( pr1 cd × pr1 ( pr2 ab ) ).

Lemma afldfracapartiscomprel :
  iscomprelrel ( eqrelcommringfrac A ( aintdomazerosubmonoid A ) )
               ( afldfracapartrelpre ).
Proof.
  intros ab cd ef gh p q.
  unfold afldfracapartrelpre.
  destruct ab as [ a b ].
  destruct b as [ b b' ].
  destruct cd as [ c d ].
  destruct d as [ d d' ].
  destruct ef as [ e f ].
  destruct f as [ f f' ].
  destruct gh as [ g h ].
  destruct h as [ h h' ].
  simpl in ×.
  apply hPropUnivalence.
  - intro u.
    apply p.
    intro p'.
    apply q.
    intro q'.
    destruct p' as [ p' j ].
    destruct p' as [ i p' ].
    destruct q' as [ q' j'].
    destruct q' as [ i' q' ].
    simpl in ×.
    assert ( a × f × d × i × h × i' # e × b × d × i × h × i') as v0.
    { assert ( a × f × d # e × b × d ) as v0.
      { apply azerormultcomp.
        + apply d'.
        + assumption. }
      assert ( a × f × d × i # e × b × d × i ) as v1
      by (apply azerormultcomp; assumption).
      assert ( a × f × d × i × h # e × b × d × i × h ) as v2
      by (apply azerormultcomp; assumption).
      apply azerormultcomp; assumption.
    }
    apply ( pr2 ( acommring_amult A ) b ).
    apply ( pr2 ( acommring_amult A ) f ).
    apply ( pr2 ( acommring_amult A ) i ).
    apply ( pr2 ( acommring_amult A ) i' ).
    assert ( a × f × d × i × h × i' = c × h × b × f × i × i' ) as l.
    { assert ( a × f × d × i × h × i' = a × d × i × f × h × i' ) as l0.
      { change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A a f ) d ) i ) h ) i' =
                 @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A a d ) i ) f ) h ) i' ).
        permute.
      }
      rewrite l0.
      rewrite j.
      change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A c b ) i ) f ) h ) i' =
               @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A c h ) b ) f ) i ) i' ).
      permute.
    }
    rewrite l in v0.
    assert ( e × b × d × i × h × i' = g × d × b × f × i × i' ) as k.
    { assert ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A e b ) d ) i ) h ) i' =
               @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A e h ) i' ) i ) b ) d ) as k0
      by permute.
      change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A e b ) d ) i ) h ) i' =
               @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A g d ) b ) f ) i ) i' ).
      rewrite k0.
      assert ( @op2 A ( @op2 A e h ) i' = @op2 A ( @op2 A g f ) i' ) as j''
      by assumption.
      rewrite j''.
      permute.
    }
    rewrite k in v0.
    assumption.
  - intro u.
    apply p.
    intro p'.
    apply q.
    intro q'.
    destruct p' as [ p' j ].
    destruct p' as [ i p' ].
    destruct q' as [ q' j' ].
    destruct q' as [ i' q' ].
    simpl in ×.
    assert ( c × h × b × f × i × i' # g × d × b × f × i × i' ) as v.
    { apply azerormultcomp.
      + apply q'.
      + apply azerormultcomp.
        × apply p'.
        × apply azerormultcomp.
          -- apply f'.
          -- apply azerormultcomp.
             ++ apply b'.
             ++ assumption.
    }
    apply ( pr2 ( acommring_amult A ) d ).
    apply ( pr2 ( acommring_amult A ) h ).
    apply ( pr2 ( acommring_amult A ) i ).
    apply ( pr2 ( acommring_amult A ) i' ).
    assert ( c × h × b × f × i × i' = a × f × d × h × i × i' ) as k.
    { assert ( c × h × b × f × i × i' = c × b × i × f × h × i' ) as k0.
      { change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A c h ) b ) f ) i ) i' =
                @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A c b ) i ) f ) h ) i' ).
        permute.
      }
      rewrite k0.
      rewrite <- j.
      change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A a d ) i ) f ) h ) i' =
               @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A a f ) d ) h ) i ) i' ).
      permute.
    }
    rewrite k in v.
    assert ( g × d × b × f × i × i' = e × b × d × h × i × i' ) as l.
    { assert ( g × d × b × f × i × i' = g × f × i' × d × i × b ) as l0.
      { change ( @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A g d ) b ) f ) i ) i' =
                 @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A g f ) i' ) d ) i ) b ).
        permute.
      }
      rewrite l0.
      rewrite <- j'.
      change (@op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A e h ) i' ) d ) i ) b =
              @op2 A ( @op2 A ( @op2 A ( @op2 A ( @op2 A e b ) d ) h ) i ) i' ).
      permute.
    }
    rewrite l in v.
    assumption.
Defined.

Definition afldfracapartrel := quotrel afldfracapartiscomprel.

Lemma isirreflafldfracapartrelpre : isirrefl afldfracapartrelpre.
Proof.
  intros ab.
  apply acommring_airrefl.
Defined.

Lemma issymmafldfracapartrelpre : issymm afldfracapartrelpre.
Proof.
  intros ab cd.
  apply ( acommring_asymm A ).
Defined.

Lemma iscotransafldfracapartrelpre : iscotrans afldfracapartrelpre.
Proof.
  intros ab cd ef p.
  destruct ab as [ a b ].
  destruct b as [ b b' ].
  destruct cd as [ c d ] .
  destruct d as [ d d' ] .
  destruct ef as [ e f ].
  destruct f as [ f f' ].
  assert ( a × f × d # e × b × d ) as v.
  { apply azerormultcomp; assumption. }
  use (hinhuniv _
    ( acommring_acotrans A ( a × f × d ) ( c × b × f ) ( e × b × d ) v )).
  intro u. intros P k.
  apply k.
  unfold afldfracapartrelpre in ×.
  simpl in ×.
  destruct u as [ left | right ].
  - apply ii1.
    apply ( pr2 ( acommring_amult A ) f ).
    assert ( @op2 A ( @op2 A a f ) d = @op2 A ( @op2 A a d ) f ) as i
    by permute.
    change ( @op2 A ( @op2 A a d ) f # @op2 A ( @op2 A c b ) f ).
    rewrite <- i.
    assumption.
  - apply ii2.
    apply ( pr2 ( acommring_amult A ) b ).
    assert ( @op2 A ( @op2 A c f ) b = @op2 A ( @op2 A c b ) f ) as i
    by permute.
    change ( @op2 A ( @op2 A c f ) b # @op2 A ( @op2 A e d ) b ).
    rewrite i.
    assert ( @op2 A ( @op2 A e d ) b = @op2 A ( @op2 A e b ) d ) as j
    by permute.
    change ( @op2 A ( @op2 A c b ) f # @op2 A ( @op2 A e d ) b ).
    rewrite j.
    assumption.
Defined.

Lemma isapartafldfracapartrel : isapart afldfracapartrel.
Proof.
  intros.
  split.
  - apply isirreflquotrel.
    exact isirreflafldfracapartrelpre.
  - split.
    + apply issymmquotrel.
      exact issymmafldfracapartrelpre.
    + apply iscotransquotrel.
      exact iscotransafldfracapartrelpre.
Defined.

Definition afldfracapart : apart ( commringfrac A (aintdomazerosubmonoid A)).
Proof.
  intros.
  unfold apart.
  split with afldfracapartrel.
  exact isapartafldfracapartrel.
Defined.

Lemma isbinapartlafldfracop1 : isbinopapartl afldfracapart op1.
Proof.
  intros.
  unfold isbinopapartl.
  assert ( ∀ a b c : commringfrac A ( aintdomazerosubmonoid A ),
    isaprop ( pr1 (afldfracapart) ( commringfracop1 A ( aintdomazerosubmonoid A ) a b)
                                  ( commringfracop1 A ( aintdomazerosubmonoid A ) a c) →
                                  pr1 (afldfracapart ) b c) ) as int.
  { intros a b c.
    apply impred.
    intro p.
    apply ( pr1 ( afldfracapart ) b c ).
  }
  apply ( setquotuniv3prop _ ( fun a b c ⇒ make_hProp _ ( int a b c ) ) ).
  intros ab cd ef p.
  destruct ab as [ a b ].
  destruct b as [ b b' ].
  destruct cd as [ c d ].
  destruct d as [ d d' ].
  destruct ef as [ e f ].
  destruct f as [ f f' ].
  unfold afldfracapart in ×.
  simpl.
  unfold afldfracapartrel.
  unfold quotrel.
  rewrite setquotuniv2comm.
  unfold afldfracapartrelpre.
  simpl.
  assert ( afldfracapartrelpre ( make_dirprod ( @op1 A ( @op2 A d a ) ( @op2 A b c ) )
             ( @op ( aintdomazerosubmonoid A ) ( tpair b b' ) ( tpair d d' ) ) )
                               ( make_dirprod ( @op1 A ( @op2 A f a ) ( @op2 A b e ) )
             ( @op ( aintdomazerosubmonoid A ) ( tpair b b' ) ( tpair f f' ) ) ) ) as u
  by apply p.
  unfold afldfracapartrelpre in u.
  simpl in u.
  rewrite 2! ( @ringrdistr A ) in u.
  do 4 rewrite <- ringassoc2 in u.
  assert ( (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A))))
           (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A))))
           (@op2 (@pr1 setwith2binop (fun X : setwith2binop ⇒
    @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X))
    (acommringtocommring (pr1aintdom A))) d a) b) f) =
           (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A))))
           (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A))))
           (@op2 (@pr1 setwith2binop (fun X : setwith2binop ⇒
     @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X))
     (acommringtocommring (pr1aintdom A))) f a) b) d) ) as i
  by permute.
  rewrite i in u.
  assert ( (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A))))
           (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A))))
           (@op2 (@pr1 setwith2binop (fun X : setwith2binop ⇒
    @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X))
    (acommringtocommring (pr1aintdom A))) b c) b) f) =
          (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A))))
          (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A))))
          (@op2 (@pr1 setwith2binop (fun X : setwith2binop ⇒
   @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X))
   (acommringtocommring (pr1aintdom A))) c f) b) b) ) as j
  by permute.
  rewrite j in u.
  assert ( (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A))))
           (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A))))
           (@op2 (@pr1 setwith2binop (fun X : setwith2binop ⇒
    @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X))
    (acommringtocommring (pr1aintdom A))) b e) b) d) =
           (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A))))
           (@op2 (pr1ring (commringtoring (acommringtocommring (pr1aintdom A))))
           (@op2 (@pr1 setwith2binop (fun X : setwith2binop ⇒
    @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X))
    (acommringtocommring (pr1aintdom A))) e d) b) b) ) as j'
  by permute.
  rewrite j' in u.
  apply ( pr2 ( acommring_amult A ) b ).
  apply ( pr2 ( acommring_amult A ) b ).
  apply ( pr1 ( acommring_aadd A) ( f × a × b × d ) ).
  assumption.
Defined.

Lemma isbinapartrafldfracop1 : isbinopapartr afldfracapart op1.
Proof.
  intros a b c.
  rewrite ringcomm1.
  rewrite ( ringcomm1 _ c ).
  apply isbinapartlafldfracop1.
Defined.

Lemma isbinapartlafldfracop2 : isbinopapartl afldfracapart op2.
Proof.
  intros.
  unfold isbinopapartl.
  assert ( ∀ a b c : commringfrac A ( aintdomazerosubmonoid A ),
    isaprop ( pr1 (afldfracapart ) ( commringfracop2 A ( aintdomazerosubmonoid A ) a b)
                                   ( commringfracop2 A ( aintdomazerosubmonoid A ) a c) →
                                   pr1 (afldfracapart ) b c) ) as int.
  { intros a b c.
    apply impred.
    intro p.
    apply ( pr1 ( afldfracapart ) b c ).
  }
  apply ( setquotuniv3prop _ ( fun a b c ⇒ make_hProp _ ( int a b c ) ) ).
  intros ab cd ef p.
  destruct ab as [ a b ].
  destruct b as [ b b' ].
  destruct cd as [ c d ].
  destruct d as [ d d' ].
  destruct ef as [ e f ].
  destruct f as [ f f' ].
  assert ( afldfracapartrelpre ( make_dirprod ( ( a × c ) )
            ( @op ( aintdomazerosubmonoid A ) ( tpair b b' ) ( tpair d d' ) ) )
                               ( make_dirprod ( a × e )
            ( @op ( aintdomazerosubmonoid A ) ( tpair b b' ) ( tpair f f' ) ) ) ) as u
  by apply p.
  unfold afldfracapart in ×.
  simpl.
  unfold afldfracapartrel.
  unfold quotrel.
  rewrite ( setquotuniv2comm ( eqrelcommringfrac A ( aintdomazerosubmonoid A ) ) ).
  unfold afldfracapartrelpre in ×.
  simpl.
  simpl in u.
  apply ( pr2 ( acommring_amult A ) a ).
  apply ( pr2 ( acommring_amult A ) b ).
  assert ( c × f × a × b =
    (@op2 (@pr1 setwith2binop (fun X : setwith2binop ⇒
        @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X))
                (acommringtocommring (pr1aintdom A)))
    (@op2 (@pr1 setwith2binop (fun X : setwith2binop ⇒
        @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X))
                (acommringtocommring (pr1aintdom A))) a c)
    (@op2 (@pr1 setwith2binop (fun X : setwith2binop ⇒
        @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X))
                (acommringtocommring (pr1aintdom A))) b f)) ) as i.
  { change ( c × f × a × b = a × c × ( b × f ) ).
    permute.
  }
  change ( c × f × a × b # e × d × a × b ).
  rewrite i.
  assert ( e × d × a × b =
    (@op2 (@pr1 setwith2binop (fun X : setwith2binop ⇒
        @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X))
                (acommringtocommring (pr1aintdom A)))
    (@op2 (@pr1 setwith2binop (fun X : setwith2binop ⇒
        @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X))
                (acommringtocommring (pr1aintdom A))) a e)
    (@op2 (@pr1 setwith2binop (fun X : setwith2binop ⇒
        @iscommringops (pr1setwith2binop X) (@op1 X) (@op2 X))
                (acommringtocommring (pr1aintdom A))) b d)) ) as i'.
  { change ( e × d × a × b = a × e × ( b × d ) ).
    permute.
  }
  rewrite i'.
  assumption.
Defined.

Lemma isbinapartrafldfracop2 : isbinopapartr (afldfracapart ) op2.
Proof.
  intros a b c.
  rewrite ringcomm2.
  rewrite ( ringcomm2 _ c ).
  apply isbinapartlafldfracop2.
Defined.

Definition afldfrac0 : acommring.
Proof.
  split with ( commringfrac A ( aintdomazerosubmonoid A ) ).
  split with afldfracapart.
  split.
  - split.
    + apply isbinapartlafldfracop1.
    + apply isbinapartrafldfracop1.
  - split.
    + apply isbinapartlafldfracop2.
    + apply isbinapartrafldfracop2.
Defined.

Definition afldfracmultinvint ( ab : A × aintdomazerosubmonoid A )
           ( is : afldfracapartrelpre ab ( make_dirprod ( @ringunel1 A )
                              ( unel ( aintdomazerosubmonoid A ) ) ) ) :
  A × aintdomazerosubmonoid A.
Proof.
  intros.
  destruct ab as [ a b ].
  destruct b as [ b b' ].
  split with b.
  simpl in is.
  split with a.
  unfold afldfracapartrelpre in is.
  simpl in is.
  change ( a # 0 ).
  rewrite ( @ringmult0x A ) in is.
  rewrite ( @ringrunax2 A ) in is.
  assumption.
Defined.

Definition afldfracmultinv ( a : afldfrac0 ) ( is : a # 0 ) :
  multinvpair afldfrac0 a.
Proof.
  intros.
  assert ( ∀ b : afldfrac0, isaprop ( b # 0 → multinvpair afldfrac0 b ) ) as int.
  { intros.
    apply impred.
    intro p.
    apply ( isapropmultinvpair afldfrac0 ).
  }
  assert ( ∀ b : afldfrac0, b # 0 → multinvpair afldfrac0 b ) as p.
  { apply ( setquotunivprop _ ( fun x0 ⇒ make_hProp _ ( int x0 ) ) ).
    intros bc q.
    destruct bc as [ b c ].
    assert ( afldfracapartrelpre ( make_dirprod b c )
      ( make_dirprod ( @ringunel1 A ) ( unel (aintdomazerosubmonoid A ) ) ) ) as is'
    by apply q.
    split with (setquotpr (eqrelcommringfrac A (aintdomazerosubmonoid A))
                              (afldfracmultinvint ( make_dirprod b c ) is' ) ).
    split.
    - change ( setquotpr ( eqrelcommringfrac A ( aintdomazerosubmonoid A ) )
        ( make_dirprod ( @op2 A ( pr1 ( afldfracmultinvint ( make_dirprod b c ) is' ) ) b )
                      ( @op ( aintdomazerosubmonoid A ) ( pr2 ( afldfracmultinvint
                                                  ( make_dirprod b c ) is' ) ) c ) ) =
      ( commringfracunel2 A ( aintdomazerosubmonoid A ) ) ).
      apply iscompsetquotpr.
      unfold commringfracunel2int.
      destruct c as [ c c' ].
      simpl.
      apply total2tohexists.
      split with ( make_carrier ( fun x : pr1 A ⇒ x # 0 ) 1 ( pr1 ( pr2 A ) ) ).
      simpl.
      rewrite 3! ( @ringrunax2 A ).
      rewrite ( @ringlunax2 A ).
      apply ( @ringcomm2 A ).
    - change ( setquotpr ( eqrelcommringfrac A ( aintdomazerosubmonoid A ) )
        ( make_dirprod ( @op2 A b ( pr1 ( afldfracmultinvint ( make_dirprod b c ) is' ) ) )
                      ( @op ( aintdomazerosubmonoid A ) c ( pr2 ( afldfracmultinvint
                                                  ( make_dirprod b c ) is' ) ) ) ) =
      ( commringfracunel2 A ( aintdomazerosubmonoid A ) ) ).
      apply iscompsetquotpr.
      destruct c as [ c c' ].
      simpl.
      apply total2tohexists.
      split with ( make_carrier ( fun x : pr1 A ⇒ x # 0 ) 1 ( pr1 ( pr2 A ) ) ).
      simpl.
      rewrite 3! ( @ringrunax2 A ).
      rewrite ( @ringlunax2 A ).
      apply ( @ringcomm2 A ).
  }
  apply p.
  assumption.
Defined.

Theorem afldfracisafld : isaafield afldfrac0.
Proof.
  intros.
  split.
  - change ( afldfracapartrel
               ( @ringunel2 ( commringfrac A (aintdomazerosubmonoid A ) ) )
               ( @ringunel1 ( commringfrac A ( aintdomazerosubmonoid A ) ) ) ).
    unfold afldfracapartrel.
    set ( aux := @op2 A ( @ringunel2 A ) ( @ringunel2 A ) #
                 @op2 A ( @ringunel1 A ) ( @ringunel2 A ) ).
    cut (pr1 aux).     + intro v.
      apply v.
    + unfold aux.
      rewrite 2! ( @ringrunax2 A ).
      apply A.
  - intros a p.
    apply afldfracmultinv.
    assumption.
Defined.

Definition afldfrac := make_afld afldfrac0 afldfracisafld.

End aint.

Close Scope ring_scope.