proposition: Lemma sum_constant : forall i k (a : X A B), 0 < k -> sum i k (fun _ => a) == a.
proof: Proof. induction k; intros. lia_false. simpl_sum_r. destruct (eq_nat_dec 0 k). subst. simpl_sum_r. auto with algebra. setoid_rewrite IHk. trivial with algebra. lia. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)