fact: Fixpoint times (x y : positive) {struct y} : positive := match x, y with | xH, _ => y | _, xH => x | xO x', xO y' => xO (xO (times x' y')) | xO x', xI y' => xO (x' + xO (times x' y')) | xI x', xO y' => xO (y' + xO (times x' y')) | xI x', xI y' => xI (x' + y' + xO (times x' y')) end.
imports: ZArith Lia