intros (G x n); elim n; simplify; [apply le_reflexive]
apply (le_transitive ???? H1);
apply (le_rewl ??? (0+(n1*x)) (zero_neutral ??));
apply fle_plusr; assumption;
qed.
intros (G x n); elim n; simplify; [apply le_reflexive]
apply (le_transitive ???? H1);
apply (le_rewl ??? (0+(n1*x)) (zero_neutral ??));
apply fle_plusr; assumption;
qed.