fact: Fixpoint diff (m n: nat) {struct m}: nat * nat := match m, n with O, n => (O, n) | m, O => (m, O) | S m1, S n1 => diff m1 n1 end.
imports: ZArith Lia Ndigits BigNumPrelude DoubleType DoubleBase CyclicAxioms DoubleCyclic