proposition: Lemma eqo_refl : forall i, eqo i i = Some (eq_refl i).
proof: Proof. unfold eqo;intros i. generalize (eqb_correct i i). rewrite eqb_refl;intros e. rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63