proposition: Lemma compat_sum_unit_add : forall x n h, compat_sum_unit h -> compat_sum_unit (add_to_sum i (is_unit_of i) x n h).
proof: Proof. unfold add_to_sum;intros; inversion H; case_eq (is_sum i (is_unit_of i) x); intros; simpl; try constructor || eauto. apply H0. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)