proposition: Theorem ratIdentityIndiscernables : forall r1 r2, r1 == r2 <-> ratDistance r1 r2 == rat0.
proof: Proof. rattac; unfold ratDistance, ratSubtract in *; rattac; unfold minRat, maxRat in *; rattac. case_eq (bleRat (RatIntro n (exist (fun n : nat => n > 0) x2 g2)) (RatIntro n0 (exist (fun n : nat => n > 0) x1 g1))); intuition. rewrite H1 in H2. rewrite H1 in H0. rattac. rewrite H1 in H2. rewrite H1 in H0. rattac. case_eq (bleRat (RatIntro n0 (exist (fun n : nat => n > 0) x0 g0)) (RatIntro n1 (exist (fun n : nat => n > 0) x g))); intuition. rewrite H0 in H1. rewrite H0 in H2. rattac. inversion e; clear e; subst. apply Nat.eq_mul_0 in H2; intuition. unfold posnatMult in *. inversion H5; clear H5; subst. assert ((RatIntro n4 (exist (fun n : nat => n > 0) x0 g0)) <= (RatIntro n3 (exist (fun n : nat => n > 0) x g))). unfold leRat. trivial. eapply nat_minus_eq. apply (leRat_mult H2). trivial. lia. rewrite H0 in H1. rewrite H0 in H2. rattac. unfold posnatMult in *. simpl in *. inversion H5; clear H5; subst. apply Nat.eq_mul_0 in e. intuition. symmetry. eapply nat_minus_eq; trivial. apply bleRat_total in H0. assert (leRat (RatIntro n4 (exist (fun n : nat => n > 0) x g)) (RatIntro n3 (exist (fun n : nat => n > 0) x0 g0))). apply H0. apply (leRat_mult H2). lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms