proposition: Lemma ratSubtract_series_map : forall n f1 f2 a1 a2, n > 0 -> sumList_rel f1 (getNats O n) a1 -> sumList_rel f2 (getNats O n) a2 -> (forall i x1 x2, f1 (S i) x1 -> f2 i x2 -> x1 == x2) -> (forall i v1 v2, f1 i v1 -> f1 i v2 -> v1 == v2) -> (forall i v1 v2, f2 i v1 -> f2 i v2 -> v1 == v2) -> (forall i v1 v2, f1 i v1 -> f2 i v2 -> v2 <= v1) -> (forall i1 i2 v1 v2, (i1 <= i2)%nat -> f1 i1 v1 -> f1 i2 v2 -> v2 <= v1) -> (forall i1 i2 v1 v2, (i1 <= i2)%nat -> f2 i1 v1 -> f2 i2 v2 -> v2 <= v1) -> forall x1 x2, f1 O x1 -> f2 (pred n) x2 -> ratSubtract a1 a2 == ratSubtract x1 x2.
proof: Proof. induction n; intuition; simpl in *. lia. inversion H0; clear H0; subst. inversion H1; clear H1; subst. destruct n; simpl in *. inversion H11; clear H11; subst. inversion H12; clear H12; subst. eapply ratSubtract_eqRat_compat. rewrite H15. rewrite H1. rewrite <- ratAdd_0_r. eauto. rewrite H17. rewrite H0. rewrite <- ratAdd_0_r. eauto. rewrite H15. rewrite H17. inversion H11; clear H11; subst. inversion H12; clear H12; subst. assert (ratSubtract r1 r0 == ratSubtract x1 r5). eapply IHn. lia. econstructor. eapply H11. eapply H18. trivial. econstructor. eapply H10. eapply H16. trivial. trivial. trivial. trivial. trivial. trivial. trivial. trivial. trivial. assert (r3 <= r2). eauto. assert (r0 <= r1). rewrite H19. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply H21. } eapply ratAdd_leRat_compat. eauto. eapply series_le. eauto. eauto. trivial. rewrite ratSubtract_ratAdd_distr. rewrite ratAdd_comm. rewrite ratSubtract_ratAdd_assoc. rewrite ratAdd_comm. rewrite ratSubtract_ratAdd_assoc. rewrite H0. assert (r2 == r5). eauto. rewrite H20. assert (x2 == r3). eauto. rewrite <- H22. assert (x2 <= r5). eauto. assert (r5 <= x1). eapply leRat_trans. eapply H5. eapply H18. trivial. eapply H6. 2:{ eauto. } 2:{ eauto. } lia. symmetry. eapply ratSubtract_partition. trivial. trivial. trivial. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation