proposition: Lemma expRat_terms : forall k n (d : posnat)(p : nz (expnat d k)), expRat (RatIntro n d) k == (expnat n k) / (expnat d k).
proof: Proof. induction k; intuition; simpl in *. symmetry. eapply num_dem_same_rat1. trivial. rewrite IHk. rewrite <- ratMult_num_den. eapply eqRat_terms. intuition. eapply posnatMult_eq. Unshelve. destruct p. econstructor. eapply mult_gt_zero_if; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms