proposition: Theorem inf_false_true : forall n m : nat, inf_egal n m = false -> inf_egal m n = true.
proof: Proof. simple induction n. intros. apply False_ind. apply diff_true_false. assumption. simple induction m. intro. trivial. intros. rewrite inf_egal_eq3. apply H. assumption. Qed.