F_ring@{} : IsCRing F. Proof. repeat split; first [change sg_op with mult; change mon_unit with 1| change sg_op with plus; change mon_unit with 0]. - apply _. - hnf. apply (F_ind3 _). intros;apply path. apply Frac.pl_assoc. - hnf. apply (F_ind _). intros;apply path, Frac.pl_0_l. - hnf. apply (F_ind _). intros;apply path, Frac.pl_0_r. - hnf. apply (F_ind _). intros;apply path, Frac.pl_neg_l. - hnf;intros. rewrite (commutativity (f:=plus)). revert x;apply (F_ind _). intros;apply path, Frac.pl_neg_l. - apply _. - apply _. - hnf; apply (F_ind3 _). intros;apply path, Frac.ml_assoc. - hnf. apply (F_ind _). intros;apply path. red;simpl. rewrite 2!mult_1_l. reflexivity. - hnf. apply (F_ind _). intros;apply path. red;simpl. rewrite 2!mult_1_r. reflexivity. - hnf; apply (F_ind2 _). intros;apply path. red;simpl. rewrite (mult_comm (num y)), (mult_comm (den y)). reflexivity. - hnf. apply (F_ind3 _). intros a b c;apply path. red;simpl. rewrite <-!(mult_assoc (num a)). rewrite <-plus_mult_distr_l. rewrite <-(mult_assoc (num a)). apply ap. rewrite (mult_comm (den a) (den c)), (mult_comm (den a) (den b)). rewrite (mult_assoc (num b)), (mult_assoc (num c)). rewrite <-plus_mult_distr_r. rewrite <-(mult_assoc _ (den a) (den a * _)). apply ap. rewrite (mult_comm (den b)), <-mult_assoc. apply ap. rewrite (mult_comm (den a)). apply associativity. Qed.
Require Import HoTT.HIT.quotient. Require Import Import Frac.