proposition: Lemma cast_diff : forall i j, i =? j = false -> cast i j = None.
proof: Proof. intros i j H;unfold cast;intros; generalize (eqb_correct i j). rewrite H;trivial. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63