proposition: Lemma step_rev_up_to {n} : List.rev (up_to n) = match n with | 0 => nil | S n' => 0::map S (List.rev (up_to n')) end.
proof: Proof. induction n; simpl; [ reflexivity | ]. etransitivity; [ rewrite IHn | reflexivity ]. destruct n; simpl; [ reflexivity | ]. rewrite map_app; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts