proposition: Lemma ratSubtract_eq_r : forall r1 r2 r3, r2 <= r1 -> r3 <= r1 -> (ratSubtract r1 r2) == (ratSubtract r1 r3) -> r2 == r3.
proof: Proof. rattac. unfold ratSubtract in *. rattac. match goal with H: (_ * (?x*_) = _ * (?x*_))%nat |- _ => eapply (@mult_same_l (x * x)); nia end. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms