proposition: Lemma exp_card_sum_mult (a b c : Card) : exp_card (b + c) a = (exp_card b a) * (exp_card c a).
proof: Proof. reduce. symmetry. apply equiv_sum_distributive. Defined.
imports: HoTT.TruncType HoTT.Classes.interfaces.abstract_algebra