Theorems · Theorem · number theory

PosNum.cmp.eq_def

∀ (x x_1 : PosNum),
  x.cmp x_1 =
    match x, x_1 with
    | PosNum.one, PosNum.one => Ordering.eq
    | x, PosNum.one => Ordering.gt
    | PosNum.one, x => Ordering.lt
    | a.bit0, b.bit0 => a.cmp b
    | a.bit0, b.bit1 => Ordering.casesOn (a.cmp b) Ordering.lt Ordering.lt Ordering.gt
    | a.bit1, b.bit0 => Ordering.casesOn (a.cmp b) Ordering.lt Ordering.gt Ordering.gt
    | a.bit1, b.bit1 => a.cmp b

Defined in

Mathlib.Data.Num.Lemmas

Cited by

1 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext