This models exact nonnegative counted sums, not floating-point rounding.
Cross multiplication compares a hand-stated rational without division;
each contributor and the asserted denominator must have positive count.
67def aosCountedMeanAgreement =
68 (lambda unrestricted firstSum : Nat .
69 (lambda unrestricted firstCount : Nat .
70 (lambda unrestricted secondSum : Nat .
71 (lambda unrestricted secondCount : Nat .
72 (lambda unrestricted numerator : Nat .
73 (lambda unrestricted denominator : Nat .
74 (naturalAnd
75 (naturalNonzero firstCount)
76 (naturalAnd
77 (naturalNonzero secondCount)
78 (naturalAnd
79 (naturalNonzero denominator)
80 (naturalEqual
81 (naturalMultiply (aosCountedMeanNumerator firstSum secondSum) denominator)
82 (naturalMultiply numerator (aosCountedMeanDenominator firstCount secondCount))))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.