fact: Definition eqo i j := (if i =? j as b return ((b = true -> i = j) -> option (i=j)) then fun Heq : true = true -> i = j => Some (Heq (eq_refl true)) else fun _ : false = true -> i = j => None) (eqb_correct i j).
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63