proposition: Lemma to_rationals_involutive: ∀ x, rationals_to_rationals Q2 Q1 (rationals_to_rationals Q1 Q2 x) = x.
proof: Proof. intros x. unfold rationals_to_rationals, compose. rewrite (jections.surjective_applied _). apply (jections.bijective_applied _). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.naturals MathClasses.interfaces.rationals MathClasses.implementations.field_of_fractions MathClasses.implementations.natpair_integers MathClasses.theory.rings MathClasses.theory.integers MathClasses.theory.dec_fields