proposition: Lemma low_tree_approx_same_inv_h : forall n (A : Set)(eqd : eq_dec A)(c : Comp A) ls t, dat_correct_h c ls n t -> forall a r, lowDistApprox_ls c a n ls r -> lowDistApproxFromTree eqd t a == r.
proof: Proof. induction 1; intuition; simpl in *. symmetry. eapply evalDet_lowDistApprox_ls_done_inv; eauto. inversion H0; clear H0; subst. destruct H1; intuition. simpl in *. rewrite <- H3. erewrite pred_count_eq_0 at 1. apply eqRat_symm. apply rat_num_0. 2:{ eapply H1. } 2:{ eapply H0. } intuition. simpl in *. intuition. subst. rewrite app_nil_r in *. eapply H; eauto. destruct H2. destruct H2. intuition. simpl in *. apply rel_map_app_inv in H3. intuition. apply rel_map_map_inv in H4. apply rel_map_map_inv in H6. eapply (pred_count_first_skip) in H2. destruct H2. destruct H2. intuition. rewrite IHdat_correct_h1. 2:{ econstructor. econstructor. intuition. eapply rel_map_eq. eapply H4. trivial. intuition. rewrite <- app_assoc. simpl. trivial. eapply H3. eapply eqRat_refl. } rewrite IHdat_correct_h2. 2:{ econstructor. econstructor. intuition. eapply rel_map_eq. eapply H6. trivial. intuition. rewrite <- app_assoc. simpl. trivial. eapply H2. eapply eqRat_refl. } rewrite <- ratMult_distrib_r. rewrite <- ratAdd_den_same. rewrite H8. rewrite <- ratMult_num_den. rewrite Nat.mul_1_r. unfold posnatMult. unfold natToPosnat. rewrite <- H5. eapply eqRat_terms; trivial. unfold natToPosnat, posnatToNat. rewrite Nat.mul_comm. simpl. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat