proposition: Lemma expRat_1 : forall n, expRat 1 n == 1.
proof: Proof. induction n; intuition; simpl in *. intuition. rewrite ratMult_1_l. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms