fact: Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = Nat.max m n := match m return fst (diff m n) + n = Nat.max m n with | 0 => match n return (n = Nat.max 0 n) with | 0 => eq_refl _ | S n0 => eq_refl _ end | S m1 => match n return (fst (diff (S m1) n) + n = Nat.max (S m1) n) with | 0 => plusn0 _ | S n1 => let v := fst (diff m1 n1) + n1 in let v1 := fst (diff m1 n1) + S n1 in eq_ind v (fun n => v1 = S n) (eq_ind v1 (fun n => v1 = n) (eq_refl v1) (S v) (plusnS _ _)) _ (diff_l _ _) end end.
imports: ZArith Lia Ndigits BigNumPrelude DoubleType DoubleBase CyclicAxioms DoubleCyclic