fact: Fixpoint mul P Q := match P, Q with | Pconst c, _ => mulC c Q | _, Pconst d => mulC d P | PX P1 v P2, PX Q1 w Q2 => add (mulX v (add (mulX w (mul P1 Q1)) (mul P1 Q2))) (add (mulX w (mul P2 Q1)) (mul P2 Q2)) end.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.additional_operations HoTT.Classes.tactics.ring_quote HoTT.Classes.theory.rings