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