fact: Definition eqs (i j : int) : {i = j} + { i <> j } := (if i =? j as b return ((b = true -> i = j) -> (b = false -> i <> j) -> {i=j} + {i <> j} ) then fun (Heq : true = true -> i = j) _ => left _ (Heq (eq_refl true)) else fun _ (Hdiff : false = false -> i <> j) => right _ (Hdiff (eq_refl false))) (eqb_correct i j) (eqb_false_correct i j).
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63